added lexical class of type variables
authornipkow
Wed Jan 05 19:29:51 1994 +0100 (1994-01-05)
changeset 21342f2b8a3581f
parent 212 b2cdb675ef44
child 214 ed6a3e2b1a33
added lexical class of type variables
src/Pure/Thy/parse.ML
src/Pure/Thy/scan.ML
     1.1 --- a/src/Pure/Thy/parse.ML	Wed Jan 05 19:27:19 1994 +0100
     1.2 +++ b/src/Pure/Thy/parse.ML	Wed Jan 05 19:29:51 1994 +0100
     1.3 @@ -3,6 +3,8 @@
     1.4      Author: 	Sonia Mahjoub / Tobias Nipkow
     1.5      Copyright   1992  TU Muenchen
     1.6  
     1.7 +    modified    Dezember 1993 by Max Breitling (type-variables added)
     1.8 +
     1.9  The parser combinators.
    1.10  Adapted from Larry Paulson's ML for the Working Programmer.
    1.11  *)
    1.12 @@ -23,6 +25,7 @@
    1.13  val nat    : (token * int) list -> string * (token * int)list 
    1.14  val stg    : (token * int) list -> string * (token * int)list 
    1.15  val txt    : (token * int) list -> string * (token * int)list 
    1.16 +val typevar: (token * int) list -> string * (token * int)list
    1.17  val >>     : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    1.18  val ||     : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b 
    1.19  val --     : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 
    1.20 @@ -66,7 +69,8 @@
    1.21    | string_of_token (Lex.Id b)  = b
    1.22    | string_of_token (Lex.Nat b) = b
    1.23    | string_of_token (Lex.Txt b) = b
    1.24 -  | string_of_token (Lex.Stg b) = b;
    1.25 +  | string_of_token (Lex.Stg b) = b
    1.26 +  | string_of_token (Lex.TypVar b) = b;
    1.27  
    1.28  fun line_err x = raise SynError(Line x);
    1.29  fun eof_err s =  raise SynError(EOF s);
    1.30 @@ -97,6 +101,10 @@
    1.31    | txt ((t,n) :: toks) = line_err ("ML text", string_of_token t, n)
    1.32    | txt _ = eof_err "ML text";
    1.33  
    1.34 +fun typevar ((Lex.TypVar b,n) :: toks) = (b, toks)
    1.35 +  | typevar ((t,n)::toks) = line_err("type variable",string_of_token t,n)
    1.36 +  | typevar _ = eof_err "type variable";
    1.37 +
    1.38  
    1.39  fun ( ph >> f) toks = let val (x, toks2) = ph toks in (f x, toks2) end;
    1.40  
     2.1 --- a/src/Pure/Thy/scan.ML	Wed Jan 05 19:27:19 1994 +0100
     2.2 +++ b/src/Pure/Thy/scan.ML	Wed Jan 05 19:29:51 1994 +0100
     2.3 @@ -3,6 +3,8 @@
     2.4      Author: 	Sonia Mahjoub / Tobias Nipkow
     2.5      Copyright   1992  TU Muenchen
     2.6  
     2.7 +    modified    December 1993 by Max Breitling (Type-variables added)
     2.8 +
     2.9  The scanner. Adapted from Larry Paulson's ML for the Working Programmer.
    2.10  *)
    2.11  
    2.12 @@ -15,6 +17,7 @@
    2.13                 | Nat of string
    2.14                 | Stg of string
    2.15                 | Txt of string
    2.16 +               | TypVar of string
    2.17  
    2.18  val scan : string list -> (token * int) list
    2.19  end;
    2.20 @@ -36,13 +39,14 @@
    2.21                 | Key of string
    2.22                 | Nat of string
    2.23                 | Stg of string
    2.24 -               | Txt of string;
    2.25 +               | Txt of string
    2.26 +               | TypVar of string;
    2.27  
    2.28  
    2.29  fun lexerr(n,s) =
    2.30      error("Lexical error on line " ^ (string_of_int n) ^ ": " ^ s);
    2.31  
    2.32 -val specials = explode"!{}@#$%^&*()+-=[]:\";',./?`_~<>|\\";
    2.33 +val specials = explode"!{}@#$%^&*()+-=[]:\";,./?`_~<>|\\";
    2.34  
    2.35  fun is_symbol c = "_" = c orelse "'" = c;
    2.36  
    2.37 @@ -71,7 +75,6 @@
    2.38         else symbolic(sy^c, cs)
    2.39    | symbolic (sy, []) = (sy, []);
    2.40  
    2.41 -
    2.42  fun stringerr(n) = lexerr(n, "No matching quote found on this line");
    2.43  
    2.44  fun is_control_chr ([],_,n) = stringerr(n)
    2.45 @@ -145,6 +148,11 @@
    2.46         else if is_digit c 
    2.47              then let val (nat , cs2) = numeric(c , cs)
    2.48                   in scanning ((Nat nat,n) :: toks , cs2, n) end
    2.49 +
    2.50 +       else if c = "'" andalso is_letter(hd cs)
    2.51 +            then let val (var, cs2) = alphanum (hd cs, tl cs)
    2.52 +                 in scanning((TypVar (c^var),n) :: toks, cs2, n) end
    2.53 +
    2.54         else if c mem specials
    2.55              then if c = "\""
    2.56                   then let val (toks', cs', n') = string (toks, cs, "", n)