# HG changeset patch
# User wenzelm
# Date 889456196 -3600
# Node ID 6aa25ee18fc41e35193907a83379c77186863812
# Parent  92e12a04dca7d75633d93563a3809cf70786432d
adapted to new scanners and baroque chars;

diff -r 92e12a04dca7 -r 6aa25ee18fc4 src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Mon Mar 09 16:09:32 1998 +0100
+++ b/src/Pure/section_utils.ML	Mon Mar 09 16:09:56 1998 +0100
@@ -38,10 +38,13 @@
 
 (** String manipulation **)
 
-(*Skipping initial blanks, find the first identifier*)
+(*Skipping initial blanks, find the first identifier*)	(* FIXME *)
 fun scan_to_id s = 
-    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
-    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
+    s |> Symbol.explode
+    |> Scan.error (Scan.finite Symbol.eof
+      (!! (fn _ => "Expected to find an identifier in " ^ s)
+        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
+    |> #1;
 
 fun is_backslash c = c = "\\";
 
@@ -56,12 +59,12 @@
        | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
        | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
        | (front, b::c::rest) => 
-	   if is_blank c   (*remove any further blanks and the following \ *)
-	   then front @ escape (tl (snd (take_prefix is_blank rest)))
+	   if Symbol.is_blank c   (*remove any further blanks and the following \ *)
+	   then front @ escape (tl (snd (take_prefix Symbol.is_blank rest)))
 	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
 
 (*Remove the first and last charaters -- presumed to be quotes*)
-val trim = implode o escape o rev o tl o rev o tl o explode;
+val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;
 
 
 (*Check for some named theory*)