Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tokenize: get exploded args;
authorwenzelm
Wed, 03 Feb 1999 17:26:53 +0100
changeset 6207 58e9f980bd4f
parent 6206 7d2204fcc1e5
child 6208 ea009b75b74e
tokenize: get exploded args;
src/Pure/Thy/thy_scan.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:27 1999 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:53 1999 +0100
@@ -13,7 +13,7 @@
   datatype token_kind =
     Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF
   val name_of_kind: token_kind -> string
-  val tokenize: Scan.lexicon -> string -> (token_kind * string * int) list
+  val tokenize: Scan.lexicon -> string list -> (token_kind * string * int) list
 end;
 
 structure ThyScan: THY_SCAN =
@@ -138,9 +138,8 @@
 
 (* tokenize *)
 
-fun tokenize lex str =
+fun tokenize lex chs =
   let
-    val chs = explode str;	(*sic!*)
     val scan_toks = Scan.repeat (scan_token lex);
     val ignore = fn (Ignore, _, _) => true | _ => false;
   in
isabelle