added SCANNER;
authorwenzelm
Mon Nov 29 12:27:29 1993 +0100 (1993-11-29)
changeset 16443506f0a98ae
parent 163 ad90d96c2ec3
child 165 793be9f1e88e
added SCANNER;
changed scan_any: no longer uses take_prefix;
src/Pure/Syntax/lexicon.ML
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Nov 29 12:25:15 1993 +0100
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 29 12:27:29 1993 +0100
     1.3 @@ -9,6 +9,24 @@
     1.4  infix 3 >>;
     1.5  infix 0 ||;
     1.6  
     1.7 +signature SCANNER =
     1.8 +sig
     1.9 +  exception LEXICAL_ERROR
    1.10 +  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    1.11 +  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
    1.12 +  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    1.13 +  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
    1.14 +  val $$ : ''a -> ''a list -> ''a * ''a list
    1.15 +  val scan_empty: 'a list -> 'b list * 'a list
    1.16 +  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
    1.17 +  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.18 +  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.19 +  val scan_end: 'a list -> 'b list * 'a list
    1.20 +  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    1.21 +  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.22 +  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.23 +end;
    1.24 +
    1.25  signature LEXICON0 =
    1.26  sig
    1.27    val is_identifier: string -> bool
    1.28 @@ -19,6 +37,7 @@
    1.29  
    1.30  signature LEXICON =
    1.31  sig
    1.32 +  include SCANNER
    1.33    include LEXICON0
    1.34    val is_xid: string -> bool
    1.35    val is_tfree: string -> bool
    1.36 @@ -44,21 +63,6 @@
    1.37    val extend_lexicon: lexicon -> string list -> lexicon
    1.38    val mk_lexicon: string list -> lexicon
    1.39    val tokenize: lexicon -> bool -> string -> token list
    1.40 -
    1.41 -  exception LEXICAL_ERROR
    1.42 -  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    1.43 -  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
    1.44 -  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    1.45 -  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
    1.46 -  val $$ : ''a -> ''a list -> ''a * ''a list
    1.47 -  val scan_empty: 'a list -> 'b list * 'a list
    1.48 -  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
    1.49 -  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.50 -  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.51 -  val scan_end: 'a list -> 'b list * 'a list
    1.52 -  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    1.53 -  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.54 -  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.55  end;
    1.56  
    1.57  functor LexiconFun(): LEXICON =
    1.58 @@ -254,7 +258,10 @@
    1.59    | scan_one pred (c :: cs) =
    1.60        if pred c then (c, cs) else raise LEXICAL_ERROR;
    1.61  
    1.62 -val scan_any = take_prefix;
    1.63 +fun scan_any _ [] = ([], [])
    1.64 +  | scan_any pred (chs as c :: cs) =
    1.65 +      if pred c then apfst (cons c) (scan_any pred cs)
    1.66 +      else ([], chs);
    1.67  
    1.68  fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;
    1.69