support ML antiquotations in Scala;
tuned -- more uniform ML vs. Scala;

--- a/src/Pure/General/antiquote.ML	Sun Feb 16 14:18:14 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Feb 16 15:38:08 2014 +0100
@@ -13,7 +13,7 @@
   val reports_of: ('a -> Position.report_text list) ->
     'a antiquote list -> Position.report_text list
   val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
-  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
+  val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
   val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
 end;
 
@@ -48,7 +48,7 @@
   Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
     Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
 
-val scan_ant =
+val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
   Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
@@ -58,10 +58,10 @@
 val scan_antiq =
   Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |--
     Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
-      (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
+      (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
-val scan_text = scan_antiq >> Antiq || scan_txt >> Text;
+val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text;
 
 end;
 
@@ -69,7 +69,7 @@
 (* read *)
 
 fun read (syms, pos) =
-  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
     SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
 

--- a/src/Pure/General/antiquote.scala	Sun Feb 16 14:18:14 2014 +0100
+++ b/src/Pure/General/antiquote.scala	Sun Feb 16 15:38:08 2014 +0100
@@ -26,13 +26,16 @@
     private val txt: Parser[String] =
       rep1("@" ~ guard(one(s => s != "{")) | many1(s => s != "@")) ^^ (x => x.mkString)
 
-    private val ant: Parser[String] =
-      quoted("\"") | (quoted("`") | (cartouche | one(s => s != "}")))
+    val antiq_other: Parser[String] =
+      many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s))
+
+    private val antiq_body: Parser[String] =
+      quoted("\"") | (quoted("`") | (cartouche | antiq_other))
 
     val antiq: Parser[String] =
-      "@{" ~ rep(ant) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
+      "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
 
-    val text: Parser[Antiquote] =
+    val antiquote: Parser[Antiquote] =
       antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))
   }
 
@@ -41,7 +44,7 @@
 
   def read(input: CharSequence): List[Antiquote] =
   {
-    Parsers.parseAll(Parsers.rep(Parsers.text), new CharSequenceReader(input)) match {
+    Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match {
       case Parsers.Success(xs, _) => xs
       case Parsers.NoSuccess(_, next) =>
         error("Malformed quotation/antiquotation source" +

--- a/src/Pure/Isar/token.scala	Sun Feb 16 14:18:14 2014 +0100
+++ b/src/Pure/Isar/token.scala	Sun Feb 16 15:38:08 2014 +0100
@@ -26,7 +26,7 @@
     val STRING = Value("string")
     val ALT_STRING = Value("back-quoted string")
     val VERBATIM = Value("verbatim text")
-    val CARTOUCHE = Value("cartouche")
+    val CARTOUCHE = Value("text cartouche")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
     val ERROR = Value("bad input")

--- a/src/Pure/ML/ml_lex.scala	Sun Feb 16 14:18:14 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sun Feb 16 15:38:08 2014 +0100
@@ -51,6 +51,13 @@
     val STRING = Value("quoted string")
     val SPACE = Value("white space")
     val COMMENT = Value("comment text")
+    val ANTIQ = Value("antiquotation")
+    val ANTIQ_START = Value("antiquotation: start")
+    val ANTIQ_STOP = Value("antiquotation: stop")
+    val ANTIQ_OTHER = Value("antiquotation: other")
+    val ANTIQ_STRING = Value("antiquotation: quoted string")
+    val ANTIQ_ALT_STRING = Value("antiquotation: back-quoted string")
+    val ANTIQ_CARTOUCHE = Value("antiquotation: text cartouche")
     val ERROR = Value("bad input")
   }
 
@@ -65,8 +72,9 @@
   /** parsers **/
 
   case object ML_String extends Scan.Line_Context
+  case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context
 
-  private object Parsers extends Scan.Parsers
+  private object Parsers extends Scan.Parsers with Antiquote.Parsers
   {
     /* string material */
 
@@ -192,13 +200,41 @@
 
       val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x))
 
+      val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x))
+
       val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x))
 
-      space | (recover_delimited |
-        (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))
+      space | (recover_delimited | (ml_antiq |
+        (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))
     }
 
 
+    /* antiquotations (line-oriented) */
+
+    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] = delimited_token | other_token
@@ -207,7 +243,9 @@
     {
       val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
 
-      ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
+      ml_string_line(ctxt) |
+        (ml_comment_line(ctxt) |
+          (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
     }
   }
 

--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 14:18:14 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 15:38:08 2014 +0100
@@ -129,6 +129,13 @@
       ML_Lex.Kind.STRING -> LITERAL1,
       ML_Lex.Kind.SPACE -> NULL,
       ML_Lex.Kind.COMMENT -> COMMENT1,
+      ML_Lex.Kind.ANTIQ -> NULL,
+      ML_Lex.Kind.ANTIQ_START -> LITERAL4,
+      ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
+      ML_Lex.Kind.ANTIQ_OTHER -> NULL,
+      ML_Lex.Kind.ANTIQ_STRING -> LITERAL1,
+      ML_Lex.Kind.ANTIQ_ALT_STRING -> LITERAL2,
+      ML_Lex.Kind.ANTIQ_CARTOUCHE -> COMMENT4,
       ML_Lex.Kind.ERROR -> INVALID
     ).withDefaultValue(NULL)
   }