# HG changeset patch
# User wenzelm
# Date 911209223 -3600
# Node ID 0022d0a913b5e462a92ddc40d6cc0680f87407ab
# Parent  1c4806b4bf43c3571060d25c1f589f8f8e08fea1
tuned usage of read;

diff -r 1c4806b4bf43 -r 0022d0a913b5 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Nov 16 10:39:30 1998 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 16 10:40:23 1998 +0100
@@ -241,7 +241,9 @@
 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
 
 fun explode_xstr str =
-  #1 (Scan.error (Scan.finite Symbol.stopper scan_str) (Symbol.explode str));
+  (case Scan.read Symbol.stopper scan_str (Symbol.explode str) of
+    Some cs => cs
+  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
 
 
 
@@ -257,7 +259,7 @@
       scan_tvar >> pair TVarSy ||
       scan_var >> pair VarSy ||
       scan_tid >> pair TFreeSy ||
-      $$ "#" ^^ scan_int >> pair NumSy ||		(* FIXME remove "#" *)
+      $$ "#" ^^ scan_int >> pair NumSy ||
       scan_longid >> pair LongIdentSy ||
       scan_xid >> pair IdentSy;
 
@@ -302,8 +304,8 @@
 (* indexname *)
 
 fun indexname cs =
-  (case Scan.error (Scan.finite Symbol.stopper (Scan.option scan_vname)) cs of
-    (Some xi, []) => xi
+  (case Scan.read Symbol.stopper scan_vname cs of
+    Some xi => xi
   | _ => error ("Lexical error in variable name: " ^ quote (implode cs)));
 
 
@@ -321,9 +323,7 @@
       $$ "?" |-- $$ "'" |-- scan_vname >> tvar ||
       $$ "?" |-- scan_vname >> var ||
       Scan.any Symbol.not_eof >> (free o implode);
-  in
-    #1 (Scan.error (Scan.finite Symbol.stopper scan) (Symbol.explode str))
-  end;
+  in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
 
 
 (* variable kinds *)
@@ -338,9 +338,7 @@
 (* read_nat *)
 
 fun read_nat str =
-  (case Scan.finite Symbol.stopper (Scan.option scan_digits1) (Symbol.explode str) of
-    (Some cs, []) => Some (#1 (Term.read_int cs))
-  | _ => None);
+  apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
 
 
 end;