tokenize: get exploded args;
authorwenzelm
Wed Feb 03 17:26:53 1999 +0100 (1999-02-03)
changeset 620758e9f980bd4f
parent 6206 7d2204fcc1e5
child 6208 ea009b75b74e
tokenize: get exploded args;
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:27 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:53 1999 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    datatype token_kind =
     1.5      Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF
     1.6    val name_of_kind: token_kind -> string
     1.7 -  val tokenize: Scan.lexicon -> string -> (token_kind * string * int) list
     1.8 +  val tokenize: Scan.lexicon -> string list -> (token_kind * string * int) list
     1.9  end;
    1.10  
    1.11  structure ThyScan: THY_SCAN =
    1.12 @@ -138,9 +138,8 @@
    1.13  
    1.14  (* tokenize *)
    1.15  
    1.16 -fun tokenize lex str =
    1.17 +fun tokenize lex chs =
    1.18    let
    1.19 -    val chs = explode str;	(*sic!*)
    1.20      val scan_toks = Scan.repeat (scan_token lex);
    1.21      val ignore = fn (Ignore, _, _) => true | _ => false;
    1.22    in