# HG changeset patch
# User wenzelm
# Date 1217957349 -7200
# Node ID d41abb7bc08a2354783aeaf372d7c1dabba43826
# Parent  c7aa4c18739db6f1972d226f754dd4fbbaadd6fe
token: maintain of source, which retains original position information;
removed count/counted, advance position via scanned source;

diff -r c7aa4c18739d -r d41abb7bc08a src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Aug 05 19:29:08 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Aug 05 19:29:09 2008 +0200
@@ -32,15 +32,14 @@
   val is_blank: token -> bool
   val is_newline: token -> bool
   val val_of: token -> string
+  val clean_value: Symbol.symbol list -> Symbol.symbol list
+  val source_of: token -> string
   val unparse: token -> string
   val text_of: token -> string * string
   val is_sid: string -> bool
   val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
-  val count: (Symbol.symbol list -> Symbol.symbol * Symbol.symbol list) ->
-    Position.T * Symbol.symbol list -> Symbol.symbol * (Position.T * Symbol.symbol list)
-  val counted: (Symbol.symbol list -> Symbol.symbol list * Symbol.symbol list) ->
-    Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
-  val scan_string: Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
+  val scan_string: Position.T * Symbol.symbol list ->
+    Symbol.symbol list * (Position.T * Symbol.symbol list)
   val scan: (Scan.lexicon * Scan.lexicon) ->
     Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
   val source: bool option -> (unit -> Scan.lexicon * Scan.lexicon) ->
@@ -62,7 +61,7 @@
   Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
   String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF;
 
-datatype token = Token of Position.range * (token_kind * string);
+datatype token = Token of (Position.range * string) * (token_kind * string);
 
 val str_of_kind =
  fn Command => "command"
@@ -87,7 +86,7 @@
 
 (* position *)
 
-fun range_of (Token (range, _)) = range;
+fun range_of (Token ((range, _), _)) = range;
 
 val position_of = #1 o range_of;
 val pos_of = Position.str_of o position_of;
@@ -95,7 +94,7 @@
 
 (* control tokens *)
 
-fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
+fun mk_eof pos = Token (((pos, Position.none), ""), (EOF, ""));
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _))) = true
@@ -151,6 +150,15 @@
 
 fun val_of (Token (_, (_, x))) = x;
 
+val clean_value = filter_out (fn s => s = Symbol.DEL);
+
+fun source_of (Token ((range, src), _)) =
+  XML.Elem (Markup.tokenN, Position.properties_of (Position.encode_range range), [XML.Text src])
+  |> YXML.string_of;
+
+
+(* unparse *)
+
 fun escape q =
   implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
 
@@ -191,21 +199,6 @@
 fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
 
 
-(* position *)
-
-local
-
-fun map_position f (scan: Symbol.symbol list -> 'a * Symbol.symbol list)  =
-  Scan.depend (fn (pos: Position.T) => scan >> (fn x => (f x pos, x)));
-
-in
-
-fun count scan = map_position Position.advance scan;
-fun counted scan = map_position (fold Position.advance) scan >> implode;
-
-end;
-
-
 (* scan symbolic idents *)
 
 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
@@ -231,21 +224,22 @@
 local
 
 val char_code =
-  count (Scan.one Symbol.is_ascii_digit) --
-  count (Scan.one Symbol.is_ascii_digit) --
-  count (Scan.one Symbol.is_ascii_digit) :|--
+  Scan.one Symbol.is_ascii_digit --
+  Scan.one Symbol.is_ascii_digit --
+  Scan.one Symbol.is_ascii_digit :|--
   (fn ((a, b), c) =>
     let val (n, _) = Library.read_int [a, b, c]
-    in if n <= 255 then Scan.succeed (chr n) else Scan.fail end);
+    in if n <= 255 then Scan.succeed [chr n, Symbol.DEL, Symbol.DEL] else Scan.fail end);
 
 fun scan_str q =
-  count ($$ "\\") |-- !!! "bad escape character in string" (count ($$ q || $$ "\\") || char_code) ||
-  count (Scan.one (fn s => s <> q andalso s <> "\\" andalso Symbol.is_regular s));
+  Scan.lift ($$ "\\") |-- !!! "bad escape character in string"
+    (Scan.lift (($$ q || $$ "\\") >> single || char_code) >> cons Symbol.DEL) ||
+  Scan.lift (Scan.one (fn s => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single);
 
 fun scan_strs q =
-  count ($$ q) |--
-    !!! "missing quote at end of string"
-      (change_prompt ((Scan.repeat (scan_str q) >> implode) --| count ($$ q)));
+  Scan.lift ($$ q) |-- !!! "missing quote at end of string"
+    (change_prompt (Scan.repeat (scan_str q) --| Scan.lift ($$ q)))
+  >> (fn body => Symbol.DEL :: flat body @ [Symbol.DEL]);
 
 in
 
@@ -258,13 +252,13 @@
 (* scan verbatim text *)
 
 val scan_verb =
-  count ($$ "*" --| Scan.ahead (~$$ "}")) ||
-  count (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
+  $$ "*" --| Scan.ahead (~$$ "}") ||
+  Scan.one (fn s => s <> "*" andalso Symbol.is_regular s);
 
 val scan_verbatim =
-  count ($$ "{") |-- count ($$ "*") |--
-    !!! "missing end of verbatim text"
-      (change_prompt ((Scan.repeat scan_verb >> implode) --| count ($$ "*") --| count ($$ "}")));
+  Scan.lift ($$ "{" |-- $$ "*") |-- !!! "missing end of verbatim text"
+    (Scan.lift (change_prompt (Scan.repeat scan_verb --| $$ "*" --| $$ "}")))
+  >> (fn body => Symbol.DEL :: Symbol.DEL :: body @ [Symbol.DEL, Symbol.DEL]);
 
 
 (* scan space *)
@@ -279,16 +273,16 @@
 (* scan nested comments *)
 
 val scan_cmt =
-  Scan.depend (fn d => count ($$ "(") ^^ count ($$ "*") >> pair (d + 1)) ||
-  Scan.depend (fn 0 => Scan.fail | d => count ($$ "*") ^^ count ($$ ")") >> pair (d - 1)) ||
-  Scan.lift (count ($$ "*" --| Scan.ahead (~$$ ")"))) ||
-  Scan.lift (count (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s)));
+  Scan.depend (fn d => $$ "(" -- $$ "*" >> (fn (a, b) => (d + 1, [a, b]))) ||
+  Scan.depend (fn 0 => Scan.fail | d => $$ "*" -- $$ ")" >> (fn (a, b) => (d - 1, [a, b]))) ||
+  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")") >> single) ||
+  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s) >> single);
 
 val scan_comment =
-  count ($$ "(") |-- count ($$ "*") |--
+  Scan.lift ($$ "(" |-- $$ "*") |--
     !!! "missing end of comment"
-      (change_prompt
-        (Scan.pass 0 (Scan.repeat scan_cmt >> implode) --| count ($$ "*") --| count ($$ ")")));
+      (Scan.lift (change_prompt (Scan.pass 0 (Scan.repeat scan_cmt) --| $$ "*" --| $$ ")")))
+  >> (fn body => Symbol.DEL :: Symbol.DEL :: flat body @ [Symbol.DEL, Symbol.DEL]);
 
 
 (* scan malformed symbols *)
@@ -301,30 +295,34 @@
 
 (* scan token *)
 
-fun token_leq ((_, x1: string), (_, x2)) = x1 <= x2;
+fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun scan (lex1, lex2) =
   let
-    val scanner = Scan.state --
+    val scanner =
       (scan_string >> pair String ||
         scan_alt_string >> pair AltString ||
         scan_verbatim >> pair Verbatim ||
         scan_comment >> pair Comment ||
-        counted scan_space >> pair Space ||
-        counted scan_malformed >> pair Malformed ||
-        Scan.lift (Scan.one Symbol.is_sync >> K (Sync, Symbol.sync)) ||
-        (Scan.max token_leq
+        Scan.lift scan_space >> pair Space ||
+        Scan.lift scan_malformed >> pair Malformed ||
+        Scan.lift (Scan.one Symbol.is_sync >> K (Sync, [Symbol.sync])) ||
+        Scan.lift ((Scan.max token_leq
           (Scan.max token_leq
-            (counted (Scan.literal lex2) >> pair Command)
-            (counted (Scan.literal lex1) >> pair Keyword))
-          (counted Syntax.scan_longid >> pair LongIdent ||
-            counted Syntax.scan_id >> pair Ident ||
-            counted Syntax.scan_var >> pair Var ||
-            counted Syntax.scan_tid >> pair TypeIdent ||
-            counted Syntax.scan_tvar >> pair TypeVar ||
-            counted Syntax.scan_nat >> pair Nat ||
-            counted scan_symid >> pair SymIdent))) -- Scan.state
-      >> (fn ((pos, (k, x)), pos') => Token ((pos, pos'), (k, x)));
+            (Scan.literal lex2 >> pair Command)
+            (Scan.literal lex1 >> pair Keyword))
+          (Syntax.scan_longid >> pair LongIdent ||
+            Syntax.scan_id >> pair Ident ||
+            Syntax.scan_var >> pair Var ||
+            Syntax.scan_tid >> pair TypeIdent ||
+            Syntax.scan_tvar >> pair TypeVar ||
+            Syntax.scan_nat >> pair Nat ||
+            scan_symid >> pair SymIdent)))) :|--
+      (fn (k, syms) => Scan.depend (fn pos =>
+        let
+          val pos' = Position.advance syms pos;
+          val x = implode (clean_value syms);
+        in Scan.succeed (pos', Token (((pos, pos'), implode syms), (k, x))) end));
 
   in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
 
@@ -335,8 +333,11 @@
 
 val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
 
-fun recover msg = Scan.state -- counted (Scan.many is_junk) -- Scan.state
-  >> (fn ((pos, s), pos') => [Token ((pos, pos'), (Error msg, s))]);
+fun recover msg = Scan.lift (Scan.many is_junk) :|-- (fn syms => Scan.depend (fn pos =>
+  let
+    val pos' = Position.advance syms pos;
+    val x = implode (clean_value syms);
+  in Scan.succeed (pos', [Token (((pos, pos'), implode syms), (Error msg, x))]) end));
 
 in
 
@@ -348,5 +349,4 @@
 
 fun source_proper src = src |> Source.filter is_proper;
 
-
 end;