Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
authorwenzelm
Mon, 27 Nov 2017 11:40:41 +0100
changeset 67095 91ffe1f8bf5c
parent 67094 4a2563645635
child 67096 e77f13a6a501
proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
src/Pure/ML/ml_lex.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML/ml_lex.scala	Mon Nov 27 10:36:43 2017 +0100
+++ b/src/Pure/ML/ml_lex.scala	Mon Nov 27 11:40:41 2017 +0100
@@ -221,6 +221,9 @@
 
     /* antiquotations (line-oriented) */
 
+    def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+      cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), c) }
+
     def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
       ctxt match {
         case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished)))
@@ -257,7 +260,8 @@
       else
         ml_string_line(ctxt) |
           (ml_comment_line(ctxt) |
-            (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
+            (ml_cartouche_line(ctxt) |
+              (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
     }
   }
isabelle