Fix the highlighting of documentation comments

idris-hackers · Oct 22, 2015 · 7c3ef7a · 7c3ef7a
1 parent 549b094
commit 7c3ef7a
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: '\\{-'