# HG changeset patch # User wenzelm # Date 850218937 -3600 # Node ID 963285471dc5bcb85800f31a80a52aca3389f8ee # Parent 4744b27cdf895f6c61cd22dcec959d47d0294a56 tokenize: no gets exploded char list; diff -r 4744b27cdf89 -r 963285471dc5 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Tue Dec 10 12:55:00 1996 +0100 +++ b/src/Pure/Syntax/lexicon.ML Tue Dec 10 12:55:37 1996 +0100 @@ -77,7 +77,7 @@ val token_assoc: (token option * 'a list) list * token -> 'a list val valued_token: token -> bool val predef_term: string -> token option - val tokenize: lexicon -> bool -> string -> token list + val tokenize: lexicon -> bool -> string list -> token list end; structure Lexicon : LEXICON = @@ -372,7 +372,7 @@ (** tokenize **) -fun tokenize lex xids str = +fun tokenize lex xids chs = let val scan_xid = if xids then $$ "_" ^^ scan_id || scan_id @@ -409,7 +409,7 @@ (None, _) => error ("Lexical error at: " ^ quote (implode chs)) | (Some (tk, s), chs') => scan (tk s :: rev_toks, chs')); in - scan ([], explode str) + scan ([], chs) end;