src/Pure/General/symbol_pos.ML
changeset 50239 fb579401dc26
parent 50201 c26369c9eda6
child 50242 56b9c792a98b
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Nov 26 21:10:42 2012 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Nov 26 21:46:04 2012 +0100
     1.3 @@ -37,6 +37,9 @@
     1.4    val range: T list -> Position.range
     1.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
     1.6    val explode: text * Position.T -> T list
     1.7 +  val scan_ident: T list -> T list * T list
     1.8 +  val is_ident: T list -> bool
     1.9 +  val is_identifier: string -> bool
    1.10  end;
    1.11  
    1.12  structure Symbol_Pos: SYMBOL_POS =
    1.13 @@ -208,6 +211,18 @@
    1.14          (Symbol.explode str) ([], Position.reset_range pos);
    1.15    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
    1.16  
    1.17 +
    1.18 +(* identifiers *)
    1.19 +
    1.20 +val scan_ident =
    1.21 +  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
    1.22 +
    1.23 +fun is_ident [] = false
    1.24 +  | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss;
    1.25 +
    1.26 +fun is_identifier s =
    1.27 +  Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none));
    1.28 +
    1.29  end;
    1.30  
    1.31  structure Basic_Symbol_Pos =   (*not open by default*)