src/Pure/General/symbol_pos.ML
changeset 62751 24e2b098bf44
parent 62529 8b7bdfc09f3b
child 62781 7ba8b944d093
     1.1 --- a/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:52:19 2016 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Mar 29 20:53:52 2016 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4    val implode: T list -> text
     1.5    val implode_range: Position.range -> T list -> text * Position.range
     1.6    val explode: text * Position.T -> T list
     1.7 +  val explode0: string -> T list
     1.8    val scan_ident: T list -> T list * T list
     1.9    val is_identifier: string -> bool
    1.10  end;
    1.11 @@ -271,6 +272,8 @@
    1.12          (Symbol.explode str) ([], Position.reset_range pos);
    1.13    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.14  
    1.15 +fun explode0 str = explode (str, Position.none);
    1.16 +
    1.17  
    1.18  (* identifiers *)
    1.19  
    1.20 @@ -289,7 +292,7 @@
    1.21  
    1.22  fun is_identifier s =
    1.23    Symbol.is_ascii_identifier s orelse
    1.24 -    (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
    1.25 +    (case try (Scan.finite stopper scan_ident) (explode0 s) of
    1.26        SOME (_, []) => true
    1.27      | _ => false);
    1.28  
    1.29 @@ -302,4 +305,3 @@
    1.30    val $$$ = Symbol_Pos.$$$;
    1.31    val ~$$$ = Symbol_Pos.~$$$;
    1.32  end;
    1.33 -