proper treatment of multi-line cartouche as rudiment of antiquotation, e.g. relevant for syntax-highlighting in Isabelle/jEdit;
authorwenzelm
Mon Nov 27 11:40:41 2017 +0100 (11 months ago)
changeset 6709591ffe1f8bf5c
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
     1.1 --- a/src/Pure/ML/ml_lex.scala	Mon Nov 27 10:36:43 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.scala	Mon Nov 27 11:40:41 2017 +0100
     1.3 @@ -221,6 +221,9 @@
     1.4  
     1.5      /* antiquotations (line-oriented) */
     1.6  
     1.7 +    def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     1.8 +      cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), c) }
     1.9 +
    1.10      def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
    1.11        ctxt match {
    1.12          case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished)))
    1.13 @@ -257,7 +260,8 @@
    1.14        else
    1.15          ml_string_line(ctxt) |
    1.16            (ml_comment_line(ctxt) |
    1.17 -            (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
    1.18 +            (ml_cartouche_line(ctxt) |
    1.19 +              (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))
    1.20      }
    1.21    }
    1.22