# HG changeset patch
# User wenzelm
# Date 1515355750 -3600
# Node ID e2575ccc0f5cbb705f860c16efb4722f741e9cb8
# Parent  fb539f83683a9f5a23f52129c21fa38d0431f232
tuned;

diff -r fb539f83683a -r e2575ccc0f5c src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sun Jan 07 21:04:51 2018 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sun Jan 07 21:09:10 2018 +0100
@@ -153,6 +153,37 @@
       comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT_CARTOUCHE, x), c) }
 
 
+    /* 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)))
+        case _ => failure("")
+      }
+
+    def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+      ctxt match {
+        case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished))
+        case _ => failure("")
+      }
+
+    def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+      context match {
+        case Antiq(ctxt) =>
+          (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context))
+           else failure("")) |
+          quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } |
+          quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } |
+          cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) }
+        case _ => failure("")
+      }
+
+
+    /* token */
+
     private def other_token: Parser[Token] =
     {
       /* identifiers */
@@ -220,38 +251,6 @@
         (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))))
     }
 
-
-    /* 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)))
-        case _ => failure("")
-      }
-
-    def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
-      ctxt match {
-        case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished))
-        case _ => failure("")
-      }
-
-    def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
-      context match {
-        case Antiq(ctxt) =>
-          (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context))
-           else failure("")) |
-          quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } |
-          quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } |
-          cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) }
-        case _ => failure("")
-      }
-
-
-    /* token */
-
     def token: Parser[Token] =
       ml_char | (ml_string | (ml_comment | (ml_comment_cartouche | other_token)))