# HG changeset patch # User wenzelm # Date 1117533209 -7200 # Node ID 727c5e32930e65517273e3b44af5555b7458c9ef # Parent 00e9ca1e7261e5170bebacd3f5651f796a0d76a2 added is_ident (from Syntax/lexicon.ML); diff -r 00e9ca1e7261 -r 727c5e32930e src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Tue May 31 11:53:28 2005 +0200 +++ b/src/Pure/General/symbol.ML Tue May 31 11:53:29 2005 +0200 @@ -39,6 +39,7 @@ val is_blank: symbol -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool + val is_ident: symbol list -> bool val beginning: int -> symbol list -> string val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a val scan_id: string list -> string * string list @@ -353,6 +354,9 @@ fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end; fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end; +fun is_ident [] = false + | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs; + (** symbol input **)