# HG changeset patch # User wenzelm # Date 1218129701 -7200 # Node ID 4569003b8813f66218eb7ed21f4162ea8f7395e3 # Parent 3ec7a4d9ef189efe1ea2fa746f8f7650bc3c92e4 simplified Antiq: regular SymbolPos.text with position; renamed read_arguments to read_antiq; tuned; diff -r 3ec7a4d9ef18 -r 4569003b8813 src/Pure/Isar/antiquote.ML --- a/src/Pure/Isar/antiquote.ML Thu Aug 07 19:21:40 2008 +0200 +++ b/src/Pure/Isar/antiquote.ML Thu Aug 07 19:21:41 2008 +0200 @@ -8,12 +8,12 @@ signature ANTIQUOTE = sig datatype antiquote = - Text of string | Antiq of (string * Position.T) * Position.T | + Text of string | Antiq of SymbolPos.text * Position.T | Open of Position.T | Close of Position.T val is_antiq: antiquote -> bool - val read: string * Position.T -> antiquote list - val read_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) -> - string * Position.T -> 'a + val read: SymbolPos.text * Position.T -> antiquote list + val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) -> + SymbolPos.text * Position.T -> 'a end; structure Antiquote: ANTIQUOTE = @@ -23,7 +23,7 @@ datatype antiquote = Text of string | - Antiq of (string * Position.T) * Position.T (*text, inner position, outer position*) | + Antiq of string * Position.T | Open of Position.T | Close of Position.T; @@ -64,21 +64,20 @@ Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; val scan_antiq = - SymbolPos.scan_position -- ($$$ "@" |-- $$$ "{" |-- + SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- T.!!! "missing closing brace of antiquotation" - (SymbolPos.scan_position -- Scan.repeat scan_ant -- SymbolPos.scan_position -- - ($$$ "}" |-- SymbolPos.scan_position))) - >> (fn (pos1, (((pos2, body), pos3), pos4)) => - Antiq ((implode (map symbol (flat body)), - Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4))); + (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos))) + >> (fn (pos1, (body, pos2)) => + let val (s, (pos, _)) = SymbolPos.implode_delim pos1 pos2 (flat body) + in Antiq (s, pos) end); in -val scan_antiquote = T.!!! "malformed quotation/antiquotation" +val scan_antiquote = (Scan.repeat1 scan_txt >> (Text o implode o map symbol o flat) || scan_antiq || - SymbolPos.scan_position --| $$$ "\\" >> Open || - SymbolPos.scan_position --| $$$ "\\" >> Close); + SymbolPos.scan_pos --| $$$ "\\" >> Open || + SymbolPos.scan_pos --| $$$ "\\" >> Close); end; @@ -87,22 +86,21 @@ fun read ("", _) = [] | read (s, pos) = - (case Scan.read SymbolPos.stopper (Scan.bulk scan_antiquote) (SymbolPos.explode (s, pos)) of + (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) (SymbolPos.explode (s, pos)) of SOME xs => (check_nesting xs; xs) | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); -(* scan_arguments *) +(* read_antiq *) -fun read_arguments lex scan (s, pos) = +fun read_antiq lex scan (s, pos) = let fun err msg = cat_error msg ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos); val res = - Source.of_string s - |> Symbol.source false - |> T.source NONE (K (lex, Scan.empty_lexicon)) pos + Source.of_list (SymbolPos.explode (s, pos)) + |> T.source' NONE (K (lex, Scan.empty_lexicon)) |> T.source_proper |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE |> Source.exhaust;