eliminated redundant is_ident -- more official is_identifier;
authorwenzelm
Fri Nov 30 15:36:51 2012 +0100 (2012-11-30)
changeset 502953d6a4135a54f
parent 50293 4eea6572896e
child 50296 dab1a3d3ba30
eliminated redundant is_ident -- more official is_identifier;
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Fri Nov 30 15:24:01 2012 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Nov 30 15:36:51 2012 +0100
     1.3 @@ -251,11 +251,11 @@
     1.4  val scan_ident =
     1.5    Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
     1.6  
     1.7 -fun is_ident [] = false
     1.8 -  | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss;
     1.9 -
    1.10  fun is_identifier s =
    1.11 -  Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none));
    1.12 +  Symbol.is_ascii_identifier s orelse
    1.13 +    (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
    1.14 +      SOME (_, []) => true
    1.15 +    | _ => false);
    1.16  
    1.17  end;
    1.18