# 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 --| $$$ "\\"; +val scan_close = Symbol_Pos.scan_pos --| $$$ "\\"; in -val scan_antiquote = - (Scan.repeat1 scan_txt >> (Text o flat) || - scan_antiq || - Symbol_Pos.scan_pos --| $$$ "\\" >> Open || - Symbol_Pos.scan_pos --| $$$ "\\" >> 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)