# HG changeset patch
# User wenzelm
# Date 1218109496 -7200
# Node ID b52c0c81dcf334548241af6e1e9b189693d3f04b
# Parent  1ae745357856160206e34590d967bd735fc42a9a
renamed scan_antiquotes to read;
renamed scan_arguments to read_arguments;
improved position handling due to SymbolPos.T;
tuned;

diff -r 1ae745357856 -r b52c0c81dcf3 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Thu Aug 07 13:44:52 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Thu Aug 07 13:44:56 2008 +0200
@@ -11,8 +11,8 @@
     Text of string | Antiq of (string * Position.T) * Position.T |
     Open of Position.T | Close of Position.T
   val is_antiq: antiquote -> bool
-  val scan_antiquotes: string * Position.T -> antiquote list
-  val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
+  val read: string * Position.T -> antiquote list
+  val read_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
     string * Position.T -> 'a
 end;
 
@@ -49,52 +49,52 @@
 
 (* scan_antiquote *)
 
+open BasicSymbolPos;
 structure T = OuterLex;
 
 local
 
-fun count scan = Scan.depend (fn pos => scan >> (fn x => (Position.advance [x] pos, x)));
-
 val scan_txt =
-  count ($$ "@" --| Scan.ahead (~$$ "{")) ||
-  count (Scan.one (fn s =>
-    s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" andalso Symbol.is_regular s));
+  $$$ "@" --| Scan.ahead (~$$$ "{") ||
+  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
+    andalso Symbol.is_regular s) >> single;
 
 val scan_ant =
-  T.scan_quoted >> implode ||
-  count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
+  T.scan_quoted ||
+  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 val scan_antiq =
-  Scan.state -- (count ($$ "@") |-- count ($$ "{") |--
+  SymbolPos.scan_position -- ($$$ "@" |-- $$$ "{" |--
     T.!!! "missing closing brace of antiquotation"
-      (Scan.state -- Scan.repeat scan_ant -- Scan.state -- (count ($$ "}") |-- Scan.state)))
+      (SymbolPos.scan_position -- Scan.repeat scan_ant -- SymbolPos.scan_position --
+        ($$$ "}" |-- SymbolPos.scan_position)))
   >> (fn (pos1, (((pos2, body), pos3), pos4)) =>
-    Antiq ((implode body, Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4)));
+    Antiq ((implode (map symbol (flat body)),
+      Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4)));
 
 in
 
-val scan_antiquote =
-  Scan.repeat1 scan_txt >> (Text o implode) ||
+val scan_antiquote = T.!!! "malformed quotation/antiquotation"
+ (Scan.repeat1 scan_txt >> (Text o implode o map symbol o flat) ||
   scan_antiq ||
-  Scan.state --| count ($$ "\\<lbrace>") >> Open ||
-  Scan.state --| count ($$ "\\<rbrace>") >> Close;
+  SymbolPos.scan_position --| $$$ "\\<lbrace>" >> Open ||
+  SymbolPos.scan_position --| $$$ "\\<rbrace>" >> Close);
 
 end;
 
 
-(* scan_antiquotes *)
+(* read *)
 
-fun scan_antiquotes (s, pos) =
-  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
-      (pos, Symbol.explode s) of
-    (xs, (_, [])) => (check_nesting xs; xs)
-  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
-      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
+fun read ("", _) = []
+  | read (s, pos) =
+      (case Scan.read SymbolPos.stopper (Scan.bulk 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 *)
 
-fun scan_arguments lex antiq (s, pos) =
+fun read_arguments lex scan (s, pos) =
   let
     fun err msg = cat_error msg
       ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
@@ -104,7 +104,7 @@
       |> Symbol.source false
       |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
       |> T.source_proper
-      |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
+      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
       |> Source.exhaust;
   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;