Merge pull request #82 from geo2a/fix-docs-highlighting

Fix the highlighting of documentation comments
idris-hackers · Oct 23, 2015 · 9616bae · 9616bae
2 parents 549b094 + 7c3ef7a
commit 9616bae
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/grammars/language-idris.cson b/grammars/language-idris.cson
@@ -24,6 +24,11 @@ patterns:
       match: '(--).*$\n?'
       comment: 'Line comment'
     }
+    {
+      name: 'comment.documentation.line.idris'
+      match: '(\\|\\|\\|).*$\n?'
+      comment: 'Line comment'
+    }
     {
       name: 'storage.type.function.idris'
       match: '\\?[-!#\\$%&\\*\\+\\.\\/<=>@\\\\\^\|~:]+|[-!#\\$%&\\*\\+\\.\\/<=>@\\\\\^\|~:\\?][-!#\\$%&\\*\\+\\.\\/<=>@\\\\\^\|~:]*'
@@ -50,11 +55,6 @@ patterns:
       match: '\\(\\)'
       name: 'constant.unit.idris'
     }
-    {
-      name: 'comment.documentation.line.idris'
-      match: '(\\|\\|\\|).*$\n?'
-      comment: 'Line comment'
-    }
     {
       name: 'comment.block.idris'
       begin: '\\{-'