--- a/src/Pure/Isar/antiquote.ML Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Isar/antiquote.ML Wed Mar 18 21:55:38 2009 +0100
@@ -7,12 +7,12 @@
signature ANTIQUOTE =
sig
datatype antiquote =
- Text of string | Antiq of SymbolPos.T list * Position.T |
+ Text of string | Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T | Close of Position.T
val is_antiq: antiquote -> bool
- val read: SymbolPos.T list * Position.T -> antiquote list
+ val read: Symbol_Pos.T list * Position.T -> antiquote list
val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
- SymbolPos.T list * Position.T -> 'a
+ Symbol_Pos.T list * Position.T -> 'a
end;
structure Antiquote: ANTIQUOTE =
@@ -22,7 +22,7 @@
datatype antiquote =
Text of string |
- Antiq of SymbolPos.T list * Position.T |
+ Antiq of Symbol_Pos.T list * Position.T |
Open of Position.T |
Close of Position.T;
@@ -48,7 +48,7 @@
(* scan_antiquote *)
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
structure T = OuterLex;
local
@@ -63,18 +63,18 @@
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
val scan_antiq =
- SymbolPos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+ Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
T.!!! "missing closing brace of antiquotation"
- (Scan.repeat scan_ant -- ($$$ "}" |-- SymbolPos.scan_pos)))
+ (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
>> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
in
val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o SymbolPos.content o flat) ||
+ (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
scan_antiq ||
- SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
- SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> Close);
+ Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
+ Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
end;
@@ -86,7 +86,7 @@
fun read ([], _) = []
| read (syms, pos) =
- (case Scan.read SymbolPos.stopper (Scan.repeat scan_antiquote) syms of
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
@@ -96,7 +96,7 @@
fun read_antiq lex scan (syms, pos) =
let
fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ SymbolPos.content syms ^ "}");
+ "@{" ^ Symbol_Pos.content syms ^ "}");
val res =
Source.of_list syms