# HG changeset patch
# User nipkow
# Date 757794591 -3600
# Node ID 42f2b8a3581fd1805a9800a90d2a6f0a2b889b00
# Parent  b2cdb675ef449e1240e1bb63a35621650cf9b64f
added lexical class of type variables

diff -r b2cdb675ef44 -r 42f2b8a3581f src/Pure/Thy/parse.ML
--- a/src/Pure/Thy/parse.ML	Wed Jan 05 19:27:19 1994 +0100
+++ b/src/Pure/Thy/parse.ML	Wed Jan 05 19:29:51 1994 +0100
@@ -3,6 +3,8 @@
     Author: 	Sonia Mahjoub / Tobias Nipkow
     Copyright   1992  TU Muenchen
 
+    modified    Dezember 1993 by Max Breitling (type-variables added)
+
 The parser combinators.
 Adapted from Larry Paulson's ML for the Working Programmer.
 *)
@@ -23,6 +25,7 @@
 val nat    : (token * int) list -> string * (token * int)list 
 val stg    : (token * int) list -> string * (token * int)list 
 val txt    : (token * int) list -> string * (token * int)list 
+val typevar: (token * int) list -> string * (token * int)list
 val >>     : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
 val ||     : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b 
 val --     : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 
@@ -66,7 +69,8 @@
   | string_of_token (Lex.Id b)  = b
   | string_of_token (Lex.Nat b) = b
   | string_of_token (Lex.Txt b) = b
-  | string_of_token (Lex.Stg b) = b;
+  | string_of_token (Lex.Stg b) = b
+  | string_of_token (Lex.TypVar b) = b;
 
 fun line_err x = raise SynError(Line x);
 fun eof_err s =  raise SynError(EOF s);
@@ -97,6 +101,10 @@
   | txt ((t,n) :: toks) = line_err ("ML text", string_of_token t, n)
   | txt _ = eof_err "ML text";
 
+fun typevar ((Lex.TypVar b,n) :: toks) = (b, toks)
+  | typevar ((t,n)::toks) = line_err("type variable",string_of_token t,n)
+  | typevar _ = eof_err "type variable";
+
 
 fun ( ph >> f) toks = let val (x, toks2) = ph toks in (f x, toks2) end;
 
diff -r b2cdb675ef44 -r 42f2b8a3581f src/Pure/Thy/scan.ML
--- a/src/Pure/Thy/scan.ML	Wed Jan 05 19:27:19 1994 +0100
+++ b/src/Pure/Thy/scan.ML	Wed Jan 05 19:29:51 1994 +0100
@@ -3,6 +3,8 @@
     Author: 	Sonia Mahjoub / Tobias Nipkow
     Copyright   1992  TU Muenchen
 
+    modified    December 1993 by Max Breitling (Type-variables added)
+
 The scanner. Adapted from Larry Paulson's ML for the Working Programmer.
 *)
 
@@ -15,6 +17,7 @@
                | Nat of string
                | Stg of string
                | Txt of string
+               | TypVar of string
 
 val scan : string list -> (token * int) list
 end;
@@ -36,13 +39,14 @@
                | Key of string
                | Nat of string
                | Stg of string
-               | Txt of string;
+               | Txt of string
+               | TypVar of string;
 
 
 fun lexerr(n,s) =
     error("Lexical error on line " ^ (string_of_int n) ^ ": " ^ s);
 
-val specials = explode"!{}@#$%^&*()+-=[]:\";',./?`_~<>|\\";
+val specials = explode"!{}@#$%^&*()+-=[]:\";,./?`_~<>|\\";
 
 fun is_symbol c = "_" = c orelse "'" = c;
 
@@ -71,7 +75,6 @@
        else symbolic(sy^c, cs)
   | symbolic (sy, []) = (sy, []);
 
-
 fun stringerr(n) = lexerr(n, "No matching quote found on this line");
 
 fun is_control_chr ([],_,n) = stringerr(n)
@@ -145,6 +148,11 @@
        else if is_digit c 
             then let val (nat , cs2) = numeric(c , cs)
                  in scanning ((Nat nat,n) :: toks , cs2, n) end
+
+       else if c = "'" andalso is_letter(hd cs)
+            then let val (var, cs2) = alphanum (hd cs, tl cs)
+                 in scanning((TypVar (c^var),n) :: toks, cs2, n) end
+
        else if c mem specials
             then if c = "\""
                  then let val (toks', cs', n') = string (toks, cs, "", n)