Merge pull request #142 from justjoheinz/feature/menu_entries

Add additional entries to the Idris main menu
idris-hackers · Jan 3, 2017 · 3c57687 · 3c57687
2 parents 020fa81 + b5f5d87
commit 3c57687
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/menus/language-idris.cson b/menus/language-idris.cson
@@ -11,6 +11,22 @@
                 'label': 'Typecheck'
                 'command': 'language-idris:typecheck'
               }
+              {
+                'label': 'Open REPL'
+                'command': 'language-idris:open-repl'
+              }
+              {
+                'label': 'Apropos'
+                'command': 'language-idris:apropos'
+              }
+              {
+                'label': 'Holes'
+                'command': 'language-idris:holes'
+              }
+              {
+                'label': 'Stop Compiler'
+                'command': 'language-idris:stop-compiler'
+              }
             ]
         ]
     }