--- 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));
--- 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)
--- 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
--- 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)