# HG changeset patch
# User wenzelm
# Date 957558542 -7200
# Node ID abc0f3722aed526639c4955aa95843bce86baea0
# Parent  7239b21e20682a76923f16dee0157fe567020852
added scan_to_id (used to be in Pure/section_utils.ML);

diff -r 7239b21e2068 -r abc0f3722aed src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri May 05 22:25:17 2000 +0200
+++ b/src/HOL/thy_syntax.ML	Fri May 05 22:29:02 2000 +0200
@@ -41,6 +41,14 @@
 
 (** (co)inductive **)
 
+(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
+fun scan_to_id s =
+    s |> Symbol.explode
+    |> Scan.error (Scan.finite Symbol.stopper
+      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
+        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
+    |> #1;
+
 fun inductive_decl coind =
   let
     val no_atts = map (mk_pair o rpair "[]");
diff -r 7239b21e2068 -r abc0f3722aed src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Fri May 05 22:25:17 2000 +0200
+++ b/src/ZF/thy_syntax.ML	Fri May 05 22:29:02 2000 +0200
@@ -27,6 +27,13 @@
 	       || list1 (name>>unenclose) >> mk_list)) 
     "[]";
 
+(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
+fun scan_to_id s =
+    s |> Symbol.explode
+    |> Scan.error (Scan.finite Symbol.stopper
+      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
+        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
+    |> #1;
 
 (*(Co)Inductive definitions theory section."*)
 fun inductive_decl coind =