# HG changeset patch
# User wenzelm
# Date 1116346244 -7200
# Node ID 670f8e4b5a98a253cefd4d412cba93bb0959e8ec
# Parent  4ef32dcbb44f62a6e43e4679827e52252ff0f364
added read_variable: optional question mark on input;
removed obsolete token_assoc;
scan_indexname: improved treatment of \<^isub> and \<^isup>;
read_var: more robust against bad input;
tuned;

diff -r 4ef32dcbb44f -r 670f8e4b5a98 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue May 17 18:10:43 2005 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue May 17 18:10:44 2005 +0200
@@ -22,6 +22,7 @@
   val string_of_vname': indexname -> string
   val indexname: string -> indexname
   val read_var: string -> term
+  val read_variable: string -> indexname option
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
@@ -60,7 +61,6 @@
   val str_of_token: token -> string
   val display_token: token -> string
   val matching_tokens: token * token -> bool
-  val token_assoc: (token option * 'a list) list * token -> 'a list
   val valued_token: token -> bool
   val predef_term: string -> token option
   val tokenize: Scan.lexicon -> bool -> string list -> token list
@@ -189,18 +189,6 @@
   | matching_tokens _ = false;
 
 
-(* token_assoc *)
-
-fun token_assoc (list, key) =
-  let
-    fun assoc [] = []
-      | assoc ((keyi, xi) :: pairs) =
-          if is_none keyi orelse matching_tokens (valOf keyi, key) then
-            assoc pairs @ xi
-          else assoc pairs;
-  in assoc list end;
-
-
 (* valued_token *)
 
 fun valued_token (Token _) = false
@@ -300,34 +288,42 @@
 
 (** scan variables **)
 
-(* scan_vname *)
+(* scan_indexname *)
+
+local
 
 fun scan_vname chrs =
   let
-    fun nat_of_chs n [] = n
-      | nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs;
+    fun nat n [] = n
+      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
 
-    val nat = nat_of_chs 0;
-
-    fun split_vname chs =
-      let val (cs, ds) = take_suffix Symbol.is_digit chs
-      in (implode cs, nat ds) end
+    fun idxname cs ds = (implode (rev cs), nat 0 ds);
+    fun chop_idx [] ds = idxname [] ds
+      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
+      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
+      | chop_idx (c :: cs) ds =
+          if Symbol.is_digit c then chop_idx cs (c :: ds)
+          else idxname (c :: cs) ds;
 
     val scan =
-      scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat) ~1;
+      scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat 0) ~1;
   in
     (case scan chrs of
-      ((cs, ~1), cs') => (split_vname cs, cs')
+      ((cs, ~1), cs') => (chop_idx (rev cs) [], cs')
     | ((cs, i), cs') => ((implode cs, i), cs'))
   end;
 
-
-(* indexname *)
+in
 
 val scan_indexname =
      $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i))
   || scan_vname;
 
+end;
+
+
+(* indexname *)
+
 fun indexname cs =
   (case Scan.read Symbol.stopper scan_indexname (Symbol.explode cs) of
     SOME xi => xi
@@ -343,9 +339,16 @@
 fun read_var str =
   let
     val scan =
-      $$ "?" |-- scan_indexname >> var ||
+      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
       Scan.any Symbol.not_eof >> (free o implode);
-  in valOf (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
+  in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
+
+
+(* read_variable *)
+
+fun read_variable str =
+  let val scan = $$ "?" |-- scan_indexname || scan_indexname
+  in Scan.read Symbol.stopper scan (Symbol.explode str) end;
 
 
 (* variable kinds *)
@@ -359,21 +362,27 @@
 
 (* read_nat *)
 
-fun read_nat str =
-  Option.map (#1 o Library.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
+fun read_nat s =
+  Option.map (#1 o Library.read_int)
+    (Scan.read Symbol.stopper scan_digits1 (Symbol.explode s));
 
 
 (* read_xnum *)
 
+local
+
 fun read_intinf cs : IntInf.int * string list =
-  let val zero = ord"0"
-      val limit = zero+10
-      fun scan (num,[]) = (num,[])
-        | scan (num, c::cs) =
-              if  zero <= ord c  andalso  ord c < limit
-              then scan(10*num + IntInf.fromInt (ord c - zero), cs)
-              else (num, c::cs)
-  in  scan(0,cs)  end;
+  let
+    val zero = ord "0";
+    val limit = zero + 10;
+    fun scan (num, []) = (num, [])
+      | scan (num, c :: cs) =
+          if zero <= ord c andalso ord c < limit
+          then scan (10 * num + IntInf.fromInt (ord c - zero), cs)
+          else (num, c :: cs)
+  in scan (0, cs) end;
+
+in
 
 fun read_xnum str =
   let
@@ -385,6 +394,8 @@
       | cs => (1, cs));
   in sign * #1 (read_intinf digs) end;
 
+end;
+
 
 (* read_ident(s) *)