src/Pure/section_utils.ML
changeset 4695 6aa25ee18fc4
parent 3974 d3c2159b75fa
child 4848 99c8d95c51d6
     1.1 --- a/src/Pure/section_utils.ML	Mon Mar 09 16:09:32 1998 +0100
     1.2 +++ b/src/Pure/section_utils.ML	Mon Mar 09 16:09:56 1998 +0100
     1.3 @@ -38,10 +38,13 @@
     1.4  
     1.5  (** String manipulation **)
     1.6  
     1.7 -(*Skipping initial blanks, find the first identifier*)
     1.8 +(*Skipping initial blanks, find the first identifier*)	(* FIXME *)
     1.9  fun scan_to_id s = 
    1.10 -    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
    1.11 -    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
    1.12 +    s |> Symbol.explode
    1.13 +    |> Scan.error (Scan.finite Symbol.eof
    1.14 +      (!! (fn _ => "Expected to find an identifier in " ^ s)
    1.15 +        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    1.16 +    |> #1;
    1.17  
    1.18  fun is_backslash c = c = "\\";
    1.19  
    1.20 @@ -56,12 +59,12 @@
    1.21         | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
    1.22         | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
    1.23         | (front, b::c::rest) => 
    1.24 -	   if is_blank c   (*remove any further blanks and the following \ *)
    1.25 -	   then front @ escape (tl (snd (take_prefix is_blank rest)))
    1.26 +	   if Symbol.is_blank c   (*remove any further blanks and the following \ *)
    1.27 +	   then front @ escape (tl (snd (take_prefix Symbol.is_blank rest)))
    1.28  	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
    1.29  
    1.30  (*Remove the first and last charaters -- presumed to be quotes*)
    1.31 -val trim = implode o escape o rev o tl o rev o tl o explode;
    1.32 +val trim = implode o escape o rev o tl o rev o tl o Symbol.explode;
    1.33  
    1.34  
    1.35  (*Check for some named theory*)