# 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 --| $$$ "\\<lbrace>" >> Open ||
-  SymbolPos.scan_position --| $$$ "\\<rbrace>" >> Close);
+  SymbolPos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
+  SymbolPos.scan_pos --| $$$ "\\<rbrace>" >> 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;