# HG changeset patch
# User wenzelm
# Date 1392556694 -3600
# Node ID 984e210d412ef4dde3019a6966f8625505cf93c8
# Parent  1585a65aad641f6880c5b526d138647bb809bd28
antiquotations within plain text: Scala version in accordance to ML;

diff -r 1585a65aad64 -r 984e210d412e src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Feb 16 13:18:08 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Sun Feb 16 14:18:14 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/antiquote.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Text with antiquotations of inner items (types, terms, theorems etc.).
+Antiquotations within plain text.
 *)
 
 signature ANTIQUOTE =
@@ -45,8 +45,8 @@
 val err_prefix = "Antiquotation lexical error: ";
 
 val scan_txt =
-  $$$ "@" --| Scan.ahead (~$$ "{") ||
-  Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single;
+  Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") ||
+    Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat;
 
 val scan_ant =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
@@ -61,7 +61,7 @@
       (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
-val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat);
+val scan_text = scan_antiq >> Antiq || scan_txt >> Text;
 
 end;
 
diff -r 1585a65aad64 -r 984e210d412e src/Pure/General/antiquote.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/antiquote.scala	Sun Feb 16 14:18:14 2014 +0100
@@ -0,0 +1,52 @@
+/*  Title:      Pure/ML/antiquote.scala
+    Author:     Makarius
+
+Antiquotations within plain text.
+*/
+
+package isabelle
+
+
+import scala.util.parsing.input.CharSequenceReader
+
+
+object Antiquote
+{
+  sealed abstract class Antiquote
+  case class Text(source: String) extends Antiquote
+  case class Antiq(source: String) extends Antiquote
+
+
+  /* parsers */
+
+  object Parsers extends Parsers
+
+  trait Parsers extends Scan.Parsers
+  {
+    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: Parser[String] =
+      "@{" ~ rep(ant) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
+
+    val text: Parser[Antiquote] =
+      antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x))
+  }
+
+
+  /* read */
+
+  def read(input: CharSequence): List[Antiquote] =
+  {
+    Parsers.parseAll(Parsers.rep(Parsers.text), new CharSequenceReader(input)) match {
+      case Parsers.Success(xs, _) => xs
+      case Parsers.NoSuccess(_, next) =>
+        error("Malformed quotation/antiquotation source" +
+          Position.here(Position.Line(next.pos.line)))
+    }
+  }
+}
+
diff -r 1585a65aad64 -r 984e210d412e src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Feb 16 13:18:08 2014 +0100
+++ b/src/Pure/build-jars	Sun Feb 16 14:18:14 2014 +0100
@@ -13,6 +13,7 @@
   Concurrent/future.scala
   Concurrent/simple_thread.scala
   Concurrent/volatile.scala
+  General/antiquote.scala
   General/bytes.scala
   General/exn.scala
   General/file.scala