# HG changeset patch
# User wenzelm
# Date 939299552 -7200
# Node ID 228283fa5de493ed7541331b88f911348f703cbf
# Parent  9ace4017ead853d90107ec18cab13c48a702727a
read_idents;

diff -r 9ace4017ead8 -r 228283fa5de4 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Oct 07 14:32:18 1999 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Oct 07 14:32:32 1999 +0200
@@ -27,6 +27,7 @@
   val skolem: string -> string
   val dest_skolem: string -> string
   val read_nat: string -> int option
+  val read_idents: string -> string list
 end;
 
 signature LEXICON =
@@ -336,4 +337,19 @@
   apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str));
 
 
+(* read_ident(s) *)
+
+fun read_idents str =
+  let
+    val blanks = Scan.any Symbol.is_blank;
+    val junk = Scan.any Symbol.not_eof;
+    val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
+  in
+    (case Scan.read Symbol.stopper idents (Symbol.explode str) of
+      Some (ids, []) => ids
+    | Some (_, bad) => error ("Bad identifier: " ^ quote (implode bad))
+    | None => error ("No identifier found in: " ^ quote str))
+  end;
+
+
 end;