# HG changeset patch
# User wenzelm
# Date 1237478211 -3600
# Node ID 1d9c9fcf8513ae1a7681be4b9c64896c425f43d2
# Parent  cbe27c4ef41709c6bb300ccf4a133fea5cf90b04
parameterized datatype antiquote and read operation;

diff -r cbe27c4ef417 -r 1d9c9fcf8513 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Thu Mar 19 15:44:14 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Thu Mar 19 16:56:51 2009 +0100
@@ -6,11 +6,16 @@
 
 signature ANTIQUOTE =
 sig
-  datatype antiquote =
-    Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T |
-    Open of Position.T | Close of Position.T
-  val is_antiq: antiquote -> bool
-  val read: Symbol_Pos.T list * Position.T -> antiquote list
+  datatype 'a antiquote =
+    Text of 'a |
+    Antiq of Symbol_Pos.T list * Position.T |
+    Open of Position.T |
+    Close of Position.T
+  val is_antiq: 'a antiquote -> bool
+  val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
+  val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
+  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
+    Symbol_Pos.T list * Position.T -> 'a antiquote list
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -18,8 +23,8 @@
 
 (* datatype antiquote *)
 
-datatype antiquote =
-  Text of Symbol_Pos.T list |
+datatype 'a antiquote =
+  Text of 'a |
   Antiq of Symbol_Pos.T list * Position.T |
   Open of Position.T |
   Close of Position.T;
@@ -44,7 +49,7 @@
   in check antiqs [] end;
 
 
-(* scan_antiquote *)
+(* scan *)
 
 open Basic_Symbol_Pos;
 
@@ -63,15 +68,15 @@
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     Symbol_Pos.!!! "missing closing brace of antiquotation"
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
-  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
+  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
+
+val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
+val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
 
 in
 
-val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o flat) ||
-  scan_antiq ||
-  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
-  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
+fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
+val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
 
 end;
 
@@ -81,9 +86,9 @@
 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
   | report_antiq _ = ();
 
-fun read ([], _) = []
-  | read (syms, pos) =
-      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
+fun read _ ([], _) = []
+  | read scanner (syms, pos) =
+      (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
         SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
diff -r cbe27c4ef417 -r 1d9c9fcf8513 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:44:14 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 16:56:51 2009 +0100
@@ -194,7 +194,7 @@
 fun eval_antiquotes (txt, pos) opt_context =
   let
     val syms = Symbol_Pos.explode (txt, pos);
-    val ants = Antiquote.read (syms, pos);
+    val ants = Antiquote.read Antiquote.scan_text (syms, pos);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
     val ((ml_env, ml_body), opt_ctxt') =
       if not (exists Antiquote.is_antiq ants)
diff -r cbe27c4ef417 -r 1d9c9fcf8513 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Mar 19 15:44:14 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Mar 19 16:56:51 2009 +0100
@@ -117,7 +117,7 @@
     else if T.is_kind T.Verbatim tok then
       let
         val (txt, pos) = T.source_position_of tok;
-        val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+        val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
         val out = implode (map output_syms_antiq ants);
       in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
     else output_syms s
diff -r cbe27c4ef417 -r 1d9c9fcf8513 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:44:14 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 16:56:51 2009 +0100
@@ -156,7 +156,7 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+    val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)