src/Pure/Isar/antiquote.ML

 *)
 
 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 =
 struct
 
 (* datatype antiquote *)
 
 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;
 
 fun is_antiq (Text _) = false
   | is_antiq _ = true;

   in check antiqs [] end;
 
 
 (* scan_antiquote *)
 
-open BasicSymbolPos;
+open Basic_Symbol_Pos;
 structure T = OuterLex;
 
 local
 
 val scan_txt =

 val scan_ant =
   T.scan_quoted ||
   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;
 
 
 (* read *)

 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
   | report_antiq _ = ();
 
 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));
 
 
 (* read_antiq *)
 
 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
       |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
       |> T.source_proper