--- 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)