src/Pure/Thy/scan.ML
changeset 213 42f2b8a3581f
parent 0 a5a9c433f639
     1.1 --- a/src/Pure/Thy/scan.ML	Wed Jan 05 19:27:19 1994 +0100
     1.2 +++ b/src/Pure/Thy/scan.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    December 1993 by Max Breitling (Type-variables added)
     1.8 +
     1.9  The scanner. Adapted from Larry Paulson's ML for the Working Programmer.
    1.10  *)
    1.11  
    1.12 @@ -15,6 +17,7 @@
    1.13                 | Nat of string
    1.14                 | Stg of string
    1.15                 | Txt of string
    1.16 +               | TypVar of string
    1.17  
    1.18  val scan : string list -> (token * int) list
    1.19  end;
    1.20 @@ -36,13 +39,14 @@
    1.21                 | Key of string
    1.22                 | Nat of string
    1.23                 | Stg of string
    1.24 -               | Txt of string;
    1.25 +               | Txt of string
    1.26 +               | TypVar of string;
    1.27  
    1.28  
    1.29  fun lexerr(n,s) =
    1.30      error("Lexical error on line " ^ (string_of_int n) ^ ": " ^ s);
    1.31  
    1.32 -val specials = explode"!{}@#$%^&*()+-=[]:\";',./?`_~<>|\\";
    1.33 +val specials = explode"!{}@#$%^&*()+-=[]:\";,./?`_~<>|\\";
    1.34  
    1.35  fun is_symbol c = "_" = c orelse "'" = c;
    1.36  
    1.37 @@ -71,7 +75,6 @@
    1.38         else symbolic(sy^c, cs)
    1.39    | symbolic (sy, []) = (sy, []);
    1.40  
    1.41 -
    1.42  fun stringerr(n) = lexerr(n, "No matching quote found on this line");
    1.43  
    1.44  fun is_control_chr ([],_,n) = stringerr(n)
    1.45 @@ -145,6 +148,11 @@
    1.46         else if is_digit c 
    1.47              then let val (nat , cs2) = numeric(c , cs)
    1.48                   in scanning ((Nat nat,n) :: toks , cs2, n) end
    1.49 +
    1.50 +       else if c = "'" andalso is_letter(hd cs)
    1.51 +            then let val (var, cs2) = alphanum (hd cs, tl cs)
    1.52 +                 in scanning((TypVar (c^var),n) :: toks, cs2, n) end
    1.53 +
    1.54         else if c mem specials
    1.55              then if c = "\""
    1.56                   then let val (toks', cs', n') = string (toks, cs, "", n)