Skip to content

Commit

Permalink
[ desc ] Update
Browse files Browse the repository at this point in the history
  • Loading branch information
ice1000 committed Jun 4, 2019
1 parent 0f0c910 commit cc833be
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 33 deletions.
2 changes: 1 addition & 1 deletion res/META-INF/change-notes.html
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
in the near future
</li>
<li>Fix a bug in CubicalTT name resolution</li>
<li>Add "Export Type Theory file to HTML" action in tool window</li>
<li>Add "Export to Clickable HTML" action in tool window</li>
</ul>
0.5.2<br/>
<ul>
Expand Down
38 changes: 8 additions & 30 deletions res/META-INF/description.html
Original file line number Diff line number Diff line change
Expand Up @@ -8,105 +8,83 @@

<h3>Features (listed for each supported language):</h3><br/>
<ul>
<li>Export supported language files as clickable HTML</li>
<li>Running (type checking) your code in supported languages</li>
<li>Live template contexts for supported languages</li>
<li>Create and iconify files for supported languages</li>
<li><a href="https://docs.rs/minitt">Mini-TT</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<ul>
<li>Mini-TT executable management</li>
<li>Live templates</li>

<li>Folding code blocks and special symbols to unicode</li>
<li>Syntax highlight, color settings page</li>
<li>Rename</li>
<li>Completion/find usages/goto declaration</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="http://www.redprl.org">RedPRL</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>RedPRL executable management</li>
<li>Folding code blocks</li>
<li>Live templates</li>

<li>Rename</li>
<li>Completion/find usages/goto declaration</li>
<li>Syntax highlight, color settings page</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://github.com/owo-lang/MLPolyR">MLPolyR</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>MLPolyR executable management</li>
<li>Folding code blocks</li>
<li>Syntax highlight</li>
<li>Language injection in Strings</li>
<li>Rename</li>
<li>Completion/find usages/goto declaration</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://github.com/owo-lang/Mini-TT">Vanilla Mini-TT</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>The <code>agdacore</code> executable management</li>
<li>Folding code blocks and special symbols to unicode</li>
<li>Live templates</li>

<li>Syntax highlight, color settings page</li>
<li>Completion/find usages/goto declaration</li>
<li>Rename</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://docs.rs/voile">Voile</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>Live templates context</li>
<li>Commenter, brace matcher</li>
<li>Syntax highlight, color settings page</li>
<li>Completion/find usages/goto declaration</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>Live templates</li>
<li>Language injection in Strings</li>
<li>Folding code blocks and layout blocks</li>
<li>Dumb completion/goto definition</li>
<li>Syntax highlighter, color settings page</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://arxiv.org/abs/1611.02108">CubicalTT</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>Live template contexts</li>
<li>Executable (cubical) management</li>
<li>Folding code blocks and imports</li>
<li>Syntax highlighter, color settings page</li>
<li>Completion/find usages/goto declaration</li>
<li>Stub indices, goto symbol (search everywhere)</li>
<li>Commenter, brace matcher</li>
<li>Create and iconify files</li>
</ul>
</li>
<li><a href="https://arxiv.org/abs/1712.01800">YaccTT</a>:<br/>
<ul>
<li>Running (type checking) your code</li>
<li>Live template contexts</li>
<li>Executable (yacctt) management</li>
<li>Create and iconify files</li>
</ul>
</li>
<li>OwO:<br/>
<ul>
<li>Live templates context</li>
<li>Create and iconify files</li>
</ul>
</li>
</ul>
2 changes: 1 addition & 1 deletion res/META-INF/plugin.xml
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@
</action>
<action
id="org.ice1000.tt.action.HtmlExportAction" class="org.ice1000.tt.action.HtmlExportAction"
text="Export Type Theory File to HTML"
text="Export to Clickable HTML"
description="Export current file supported by Dependently-Typed Lambda Calculus to clickable HTML">
<add-to-group group-id="ToolsMenu" anchor="last"/>
</action>
Expand Down
2 changes: 1 addition & 1 deletion src/org/ice1000/tt/action/html-export.kt
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ object HtmlExportSupport {
if (infoClasses != null) classes = infoClasses
val infoHref = info.href
val text = element.text
if (intoHref == "??") {
if (infoHref == "??") {
title = "Failed to find the declaration of $text"
indicator.text = "Token $text (Failed)"
} else if (infoHref != null) {
Expand Down

0 comments on commit cc833be

Please sign in to comment.