src/Pure/Syntax/lexicon.ML
author wenzelm
Fri, 30 Jan 1998 11:31:21 +0100
changeset 4587 6bce9ef27d7e
parent 4247 9bba9251bb4d
child 4703 a50ab39756db
permissions -rw-r--r--
added read_var;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/lexicon.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
     5
Scanner combinators and the main lexer (for terms and types).
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     6
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     8
infix 5 -- ^^;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     9
infix 3 >>;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    10
infix 0 ||;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
164
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    12
signature SCANNER =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    13
sig
164
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    14
  exception LEXICAL_ERROR
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    15
  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    16
  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    17
  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    18
  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    19
  val $$ : ''a -> ''a list -> ''a * ''a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    20
  val scan_empty: 'a list -> 'b list * 'a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    21
  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    22
  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    23
  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    24
  val scan_end: 'a list -> 'b list * 'a list
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    25
  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    26
  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    27
  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    28
  val max_of: ('a -> ('b * string) * 'a) -> ('a -> ('b * string) * 'a)
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    29
    -> 'a -> ('b * string) option * 'a
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    30
  val scan_id: string list -> string * string list
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    31
  val scan_longid: string list -> string * string list
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    32
  val scan_tid: string list -> string * string list
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    33
  val scan_nat: string list -> string * string list
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    34
  type lexicon
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    35
  val dest_lexicon: lexicon -> string list
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    36
  val empty_lexicon: lexicon
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    37
  val extend_lexicon: lexicon -> string list -> lexicon
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    38
  val make_lexicon: string list -> lexicon
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    39
  val merge_lexicons: lexicon -> lexicon -> lexicon
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
    40
  val scan_literal: lexicon -> string list -> string * string list
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    41
end;
164
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    42
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
signature LEXICON0 =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    44
sig
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val is_identifier: string -> bool
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    46
  val implode_xstr: string list -> string
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    47
  val explode_xstr: string -> string list
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
  val string_of_vname: indexname -> string
2583
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
    49
  val string_of_vname': indexname -> string
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
  val scan_varname: string list -> indexname * string list
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    51
  val scan_var: string -> term
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    52
  val const: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    53
  val free: string -> term
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    54
  val var: indexname -> term
4587
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
    55
  val read_var: string -> string * int
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    56
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
signature LEXICON =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    59
sig
164
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
    60
  include SCANNER
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    61
  include LEXICON0
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    62
  val is_xid: string -> bool
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
    63
  val is_tid: string -> bool
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    64
  datatype token =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    65
    Token of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    66
    IdentSy of string |
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    67
    LongIdentSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    68
    VarSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    69
    TFreeSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    70
    TVarSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    71
    NumSy of string |
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    72
    StrSy of string |
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    73
    EndToken
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    74
  val idT: typ
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    75
  val longidT: typ
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    76
  val varT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    77
  val tidT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    78
  val tvarT: typ
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    79
  val terminals: string list
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    80
  val is_terminal: string -> bool
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    81
  val str_of_token: token -> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    82
  val display_token: token -> string
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    83
  val matching_tokens: token * token -> bool
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
    84
  val token_assoc: (token option * 'a list) list * token -> 'a list
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    85
  val valued_token: token -> bool
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    86
  val predef_term: string -> token option
2363
963285471dc5 tokenize: no gets exploded char list;
wenzelm
parents: 1507
diff changeset
    87
  val tokenize: lexicon -> bool -> string list -> token list
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    88
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
1507
f600215b6ea7 Elimination of fully-functorial style.
paulson
parents: 1143
diff changeset
    90
structure Lexicon : LEXICON =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    93
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    94
(** is_identifier etc. **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    95
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    96
fun is_ident [] = false
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    97
  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    98
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    99
val is_identifier = is_ident o explode;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   100
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   101
fun is_xid s =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   102
  (case explode s of
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   103
    "_" :: cs => is_ident cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   104
  | cs => is_ident cs);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   105
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   106
fun is_tid s =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   107
  (case explode s of
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   108
    "'" :: cs => is_ident cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   109
  | _ => false);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   110
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   113
(** string_of_vname **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   115
fun string_of_vname (x, i) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   116
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   117
    val si = string_of_int i;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   118
  in
1143
0dfb8b437f5d Now string_of_vname checks for the empty variable name,
lcp
parents: 550
diff changeset
   119
    (if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
0dfb8b437f5d Now string_of_vname checks for the empty variable name,
lcp
parents: 550
diff changeset
   120
     else if i = 0 then "?" ^ x
0dfb8b437f5d Now string_of_vname checks for the empty variable name,
lcp
parents: 550
diff changeset
   121
     else "?" ^ x ^ si)
0dfb8b437f5d Now string_of_vname checks for the empty variable name,
lcp
parents: 550
diff changeset
   122
    handle LIST _ => "?NULL_VARIABLE." ^ si
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   123
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
2583
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
   125
fun string_of_vname' (xi as (x, i)) =
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
   126
  if i < 0 then x else string_of_vname xi;
690835a06cf2 added string_of_vname' (treats neg. index as free);
wenzelm
parents: 2363
diff changeset
   127
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   128
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   130
(** datatype token **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   132
datatype token =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   133
  Token of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   134
  IdentSy of string |
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   135
  LongIdentSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   136
  VarSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   137
  TFreeSy of string |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   138
  TVarSy of string |
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   139
  NumSy of string |
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   140
  StrSy of string |
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   141
  EndToken;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   144
(* terminal arguments *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   146
val idT = Type ("id", []);
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   147
val longidT = Type ("longid", []);
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   148
val varT = Type ("var", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   149
val tidT = Type ("tid", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   150
val tvarT = Type ("tvar", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   152
val terminals = ["id", "longid", "var", "tid", "tvar", "xnum", "xstr"];
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   153
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   154
fun is_terminal s = s mem terminals;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   155
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   157
(* str_of_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   159
fun str_of_token (Token s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   160
  | str_of_token (IdentSy s) = s
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   161
  | str_of_token (LongIdentSy s) = s
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   162
  | str_of_token (VarSy s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   163
  | str_of_token (TFreeSy s) = s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   164
  | str_of_token (TVarSy s) = s
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   165
  | str_of_token (NumSy s) = s
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   166
  | str_of_token (StrSy s) = s
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   167
  | str_of_token EndToken = "EOF";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   169
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   170
(* display_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   172
fun display_token (Token s) = quote s
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   173
  | display_token (IdentSy s) = "id(" ^ s ^ ")"
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   174
  | display_token (LongIdentSy s) = "longid(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   175
  | display_token (VarSy s) = "var(" ^ s ^ ")"
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   176
  | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   177
  | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   178
  | display_token (NumSy s) = "xnum(" ^ s ^ ")"
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   179
  | display_token (StrSy s) = "xstr(" ^ s ^ ")"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   180
  | display_token EndToken = "";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   182
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   183
(* matching_tokens *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   185
fun matching_tokens (Token x, Token y) = (x = y)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   186
  | matching_tokens (IdentSy _, IdentSy _) = true
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   187
  | matching_tokens (LongIdentSy _, LongIdentSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   188
  | matching_tokens (VarSy _, VarSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   189
  | matching_tokens (TFreeSy _, TFreeSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   190
  | matching_tokens (TVarSy _, TVarSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   191
  | matching_tokens (NumSy _, NumSy _) = true
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   192
  | matching_tokens (StrSy _, StrSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   193
  | matching_tokens (EndToken, EndToken) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   194
  | matching_tokens _ = false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   197
(* token_assoc *)
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   198
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   199
fun token_assoc (list, key) =
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   200
  let
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   201
    fun assoc [] = []
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   202
      | assoc ((keyi, xi) :: pairs) =
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   203
          if is_none keyi orelse matching_tokens (the keyi, key) then
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   204
            assoc pairs @ xi
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   205
          else assoc pairs;
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   206
  in assoc list end;
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   207
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 237
diff changeset
   208
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   209
(* valued_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   211
fun valued_token (Token _) = false
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   212
  | valued_token (IdentSy _) = true
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   213
  | valued_token (LongIdentSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   214
  | valued_token (VarSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   215
  | valued_token (TFreeSy _) = true
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   216
  | valued_token (TVarSy _) = true
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   217
  | valued_token (NumSy _) = true
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   218
  | valued_token (StrSy _) = true
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   219
  | valued_token EndToken = false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   222
(* predef_term *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   224
fun predef_term "id" = Some (IdentSy "id")
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   225
  | predef_term "longid" = Some (LongIdentSy "longid")
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   226
  | predef_term "var" = Some (VarSy "var")
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   227
  | predef_term "tid" = Some (TFreeSy "tid")
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   228
  | predef_term "tvar" = Some (TVarSy "tvar")
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   229
  | predef_term "xnum" = Some (NumSy "xnum")
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   230
  | predef_term "xstr" = Some (StrSy "xstr")
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   231
  | predef_term _ = None;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   234
(*  xstr tokens *)
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   235
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   236
fun implode_xstr cs = enclose "''" "''" (implode cs);
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   237
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   238
fun explode_xstr str =
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   239
  rev (tl (tl (rev (tl (tl (explode str))))));
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   240
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   241
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   243
(** datatype lexicon **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   244
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   245
datatype lexicon =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   246
  Empty |
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   247
  Branch of string * string * lexicon * lexicon * lexicon;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   248
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   249
val no_token = "";
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   250
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   251
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   252
(* dest_lexicon *)
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   253
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   254
fun dest_lexicon Empty = []
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   255
  | dest_lexicon (Branch (_, "", lt, eq, gt)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   256
      dest_lexicon eq @ dest_lexicon lt @ dest_lexicon gt
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   257
  | dest_lexicon (Branch (_, str, lt, eq, gt)) =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   258
      str :: (dest_lexicon eq @ dest_lexicon lt @ dest_lexicon gt);
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   259
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   260
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   261
(* empty, extend, make, merge lexicons *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   262
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   263
val empty_lexicon = Empty;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   264
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   265
fun extend_lexicon lexicon strs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   267
    fun ext (lex, s) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   268
      let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   269
        fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   270
              if c < d then Branch (d, a, add lt chs, eq, gt)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   271
              else if c > d then Branch (d, a, lt, eq, add gt chs)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   272
              else Branch (d, if null cs then s else a, lt, add eq cs, gt)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   273
          | add Empty [c] =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   274
              Branch (c, s, Empty, Empty, Empty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   275
          | add Empty (c :: cs) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   276
              Branch (c, no_token, Empty, add Empty cs, Empty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   277
          | add lex [] = lex;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   278
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   279
        val cs = explode s;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   280
      in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   281
        if exists is_blank cs then
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   282
          sys_error ("extend_lexicon: blank in delimiter " ^ quote s)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   283
        else add lex cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   284
      end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   285
  in
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   286
    foldl ext (lexicon, strs \\ dest_lexicon lexicon)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   287
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   288
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   289
val make_lexicon = extend_lexicon empty_lexicon;
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   290
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   291
fun merge_lexicons lex1 lex2 =
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   292
  let
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   293
    val strs1 = dest_lexicon lex1;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   294
    val strs2 = dest_lexicon lex2;
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   295
  in
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   296
    if strs2 subset strs1 then lex1
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   297
    else if strs1 subset strs2 then lex2
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   298
    else extend_lexicon lex1 strs2
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   299
  end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   300
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   301
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   302
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   303
(** scanners **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   304
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   305
exception LEXICAL_ERROR;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   306
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   308
(* scanner combinators *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   309
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   310
fun (scan >> f) cs = apfst f (scan cs);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   311
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   312
fun (scan1 || scan2) cs = scan1 cs handle LEXICAL_ERROR => scan2 cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   313
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   314
fun (scan1 -- scan2) cs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   315
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   316
    val (x, cs') = scan1 cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   317
    val (y, cs'') = scan2 cs';
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   318
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   319
    ((x, y), cs'')
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   320
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   321
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   322
fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   323
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   324
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   325
(* generic scanners *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   326
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   327
fun $$ _ [] = raise LEXICAL_ERROR
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   328
  | $$ a (c :: cs) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   329
      if a = c then (c, cs) else raise LEXICAL_ERROR;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   330
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   331
fun scan_empty cs = ([], cs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   333
fun scan_one _ [] = raise LEXICAL_ERROR
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   334
  | scan_one pred (c :: cs) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   335
      if pred c then (c, cs) else raise LEXICAL_ERROR;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   336
164
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
   337
fun scan_any _ [] = ([], [])
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
   338
  | scan_any pred (chs as c :: cs) =
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
   339
      if pred c then apfst (cons c) (scan_any pred cs)
43506f0a98ae added SCANNER;
wenzelm
parents: 18
diff changeset
   340
      else ([], chs);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   341
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   342
fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   343
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   344
fun scan_rest cs = (cs, []);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   345
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   346
fun scan_end [] = ([], [])
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   347
  | scan_end _ = raise LEXICAL_ERROR;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   348
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   349
fun optional scan = scan >> Some || scan_empty >> K None;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   350
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   351
fun repeat scan cs = (scan -- repeat scan >> op :: || scan_empty) cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   352
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   353
fun repeat1 scan = scan -- repeat scan >> op ::;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   354
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   355
fun max_of scan1 scan2 cs =
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   356
  (case (optional scan1 cs, optional scan2 cs) of
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   357
    (tok1, (None, _)) => tok1
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   358
  | ((None, _), tok2) => tok2
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   359
  | (tok1 as (Some (_, s1), _), tok2 as (Some (_, s2), _)) =>
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   360
      if size s1 >= size s2 then tok1 else tok2);
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   361
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   362
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   363
(* other scanners *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   364
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   365
val scan_letter_letdigs = scan_one is_letter -- scan_any is_letdig >> op ::;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   366
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   367
val scan_digits1 = scan_any1 is_digit;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   368
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   369
val scan_id = scan_letter_letdigs >> implode;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   371
val scan_longid = scan_id ^^ (repeat1 ($$ "." ^^ scan_id) >> implode);
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   372
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   373
val scan_id_nat =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   374
  scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K "");
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   375
376
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   376
val scan_tid = $$ "'" ^^ scan_id;
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   377
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   378
val scan_nat = scan_digits1 >> implode;
d3d01131470f extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents: 330
diff changeset
   379
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   380
val scan_int = $$ "~" ^^ scan_nat || scan_nat;
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   381
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   382
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   383
(* scan_literal *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   384
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   385
fun scan_literal lex chrs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   386
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   387
    fun scan_lit _ s_cs [] = s_cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   388
      | scan_lit Empty s_cs _ = s_cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   389
      | scan_lit (Branch (d, a, lt, eq, gt)) s_cs (chs as c :: cs) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   390
          if c < d then scan_lit lt s_cs chs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   391
          else if c > d then scan_lit gt s_cs chs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   392
          else scan_lit eq (if a = no_token then s_cs else Some (a, cs)) cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   393
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   394
    (case scan_lit lex None chrs of
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   395
      None => raise LEXICAL_ERROR
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   396
    | Some s_cs => s_cs)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   397
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   398
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   399
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   400
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   401
(** tokenize **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   402
2363
963285471dc5 tokenize: no gets exploded char list;
wenzelm
parents: 1507
diff changeset
   403
fun tokenize lex xids chs =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   404
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   405
    val scan_xid =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   406
      if xids then $$ "_" ^^ scan_id || scan_id
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   407
      else scan_id;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   408
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   409
    val scan_lit = scan_literal lex >> pair Token;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   410
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   411
    val scan_val =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   412
      $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy ||
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   413
      $$ "?" ^^ scan_id_nat >> pair VarSy ||
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   414
      $$ "'" ^^ scan_id >> pair TFreeSy ||
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   415
      $$ "#" ^^ scan_int >> pair NumSy ||
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   416
      scan_longid >> pair LongIdentSy ||
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   417
      scan_xid >> pair IdentSy;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   418
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   419
    fun scan_str ("'" :: "'" :: cs) = ([], cs)
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   420
      | scan_str ("\\" :: c :: cs) = apfst (cons c) (scan_str cs)
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   421
      | scan_str (c :: cs) = apfst (cons c) (scan_str cs)
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   422
      | scan_str [] = raise ERROR;
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   423
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   424
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   425
    fun scan (rev_toks, []) = rev (EndToken :: rev_toks)
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   426
      | scan (rev_toks, chs as "'" :: "'" :: cs) =
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   427
          let
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   428
            val (cs', cs'') = scan_str cs handle ERROR =>
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   429
              error ("Lexical error: missing quotes at end of string " ^
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   430
                quote (implode chs));
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   431
          in
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   432
            scan (StrSy (implode_xstr cs') :: rev_toks, cs'')
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   433
          end
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   434
      | scan (rev_toks, chs as c :: cs) =
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   435
          if is_blank c then scan (rev_toks, cs)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   436
          else
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   437
            (case max_of scan_lit scan_val chs of
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   438
              (None, _) => error ("Lexical error at: " ^ quote (implode chs))
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   439
            | (Some (tk, s), chs') => scan (tk s :: rev_toks, chs'));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   440
  in
2363
963285471dc5 tokenize: no gets exploded char list;
wenzelm
parents: 1507
diff changeset
   441
    scan ([], chs)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   442
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   443
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   444
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   445
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   446
(** scan variables **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   447
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   448
(* scan_vname *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   449
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   450
fun scan_vname chrs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   451
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   452
    fun nat_of_chs n [] = n
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   453
      | nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   454
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   455
    val nat_of = nat_of_chs 0;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   456
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   457
    fun split_vname chs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   458
      let val (cs, ds) = take_suffix is_digit chs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   459
      in (implode cs, nat_of ds) end
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   460
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   461
    val scan =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   462
      scan_letter_letdigs --
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   463
        ($$ "." -- scan_digits1 >> (nat_of o #2) || scan_empty >> K ~1);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   464
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   465
    (case scan chrs of
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   466
      ((cs, ~1), cs') => (split_vname cs, cs')
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   467
    | ((cs, i), cs') => ((implode cs, i), cs'))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   468
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   469
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   470
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   471
(* scan_varname *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   472
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   473
fun scan_varname chs =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   474
  scan_vname chs handle LEXICAL_ERROR
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   475
    => error ("scan_varname: bad varname " ^ quote (implode chs));
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   476
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   477
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   478
(* scan_var *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   479
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   480
fun const c = Const (c, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   481
fun free x = Free (x, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   482
fun var xi = Var (xi, dummyT);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   483
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   484
fun scan_var str =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   485
  let
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   486
    fun tvar (x, i) = var ("'" ^ x, i);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   487
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   488
    val scan =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   489
      $$ "?" -- $$ "'" -- scan_vname -- scan_end >> (tvar o #2 o #1) ||
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   490
      $$ "?" -- scan_vname -- scan_end >> (var o #2 o #1) ||
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   491
      scan_rest >> (free o implode);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   492
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   493
    #1 (scan (explode str))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   494
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
   496
4587
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   497
(* read_var *)
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   498
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   499
fun read_var str =
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   500
  let val scan = $$ "?" -- scan_vname -- scan_end >> (#2 o #1) in
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   501
    #1 (scan (explode str)) handle LEXICAL_ERROR
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   502
      => error ("Bad variable " ^ quote str)
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   503
  end;
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   504
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   505
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
end;