src/Pure/Syntax/lexicon.ML
author wenzelm
Tue, 13 Aug 2013 17:26:22 +0200
changeset 53016 fa9c38891cf2
parent 52920 4539e4a06339
child 54732 b01bb3d09928
permissions -rw-r--r--
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
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
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
     4
Lexer for the inner Isabelle syntax (terms and types).
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
     7
signature LEXICON =
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
     8
sig
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
     9
  structure Syntax:
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    10
  sig
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    11
    val const: string -> term
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    12
    val free: string -> term
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    13
    val var: indexname -> term
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    14
  end
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    15
  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    16
  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    17
  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    18
  val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    19
  val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 39510
diff changeset
    20
  val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    21
  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    22
  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    23
  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    24
  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
    25
  val is_tid: string -> bool
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    26
  datatype token_kind =
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    27
    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
    28
    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    29
  datatype token = Token of token_kind * string * Position.range
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
    30
  val str_of_token: token -> string
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
    31
  val pos_of_token: token -> Position.T
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
    32
  val is_proper: token -> bool
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    33
  val mk_eof: Position.T -> token
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    34
  val eof: token
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    35
  val is_eof: token -> bool
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
    36
  val stopper: token Scan.stopper
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    37
  val idT: typ
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
    38
  val longidT: typ
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    39
  val varT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    40
  val tidT: typ
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
    41
  val tvarT: typ
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    42
  val terminals: string list
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    43
  val is_terminal: string -> bool
49821
d15fe10593ff clarified output token markup (see also bc22daeed49e);
wenzelm
parents: 48992
diff changeset
    44
  val literal_markup: string -> Markup.T
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44706
diff changeset
    45
  val report_of_token: token -> Position.report
39510
d9f5f01faa1b Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents: 39507
diff changeset
    46
  val reported_token_range: Proof.context -> token -> string
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    47
  val matching_tokens: token * token -> bool
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    48
  val valued_token: token -> bool
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
    49
  val predef_term: string -> token option
46483
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
    50
  val implode_str: string list -> string
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
    51
  val explode_str: string -> string list
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    52
  val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    53
  val read_indexname: string -> indexname
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    54
  val read_var: string -> term
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    55
  val read_variable: string -> indexname option
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    56
  val read_nat: string -> int option
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    57
  val read_int: string -> int option
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    58
  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    59
  val read_float: string -> {mant: int, exp: int}
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    60
  val mark_class: string -> string val unmark_class: string -> string
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    61
  val mark_type: string -> string val unmark_type: string -> string
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    62
  val mark_const: string -> string val unmark_const: string -> string
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    63
  val mark_fixed: string -> string val unmark_fixed: string -> string
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    64
  val unmark:
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    65
   {case_class: string -> 'a,
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    66
    case_type: string -> 'a,
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    67
    case_const: string -> 'a,
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    68
    case_fixed: string -> 'a,
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    69
    case_default: string -> 'a} -> string -> 'a
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    70
  val is_marked: string -> bool
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    71
  val dummy_type: term
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
    72
  val fun_type: term
4247
9bba9251bb4d added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents: 3828
diff changeset
    73
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
14679
6ed90bd68eda added is_ascii_identifier;
wenzelm
parents: 13808
diff changeset
    75
structure Lexicon: LEXICON =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    78
(** syntaxtic terms **)
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    79
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    80
structure Syntax =
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    81
struct
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    82
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    83
fun const c = Const (c, dummyT);
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    84
fun free x = Free (x, dummyT);
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    85
fun var xi = Var (xi, dummyT);
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    86
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    87
end;
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    88
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    89
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
    90
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    91
(** basic scanners **)
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
    92
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
    93
open Basic_Symbol_Pos;
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    94
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43432
diff changeset
    95
fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    96
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
    97
val scan_id = Symbol_Pos.scan_ident;
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    98
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
    99
val scan_tid = $$$ "'" @@@ scan_id;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   100
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   101
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   102
val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   103
val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   104
val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   105
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   106
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   107
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   108
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   109
val scan_var = $$$ "?" @@@ scan_id_nat;
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   110
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   111
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   112
fun is_tid s =
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   113
  (case try (unprefix "'") s of
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   114
    SOME s' => Symbol_Pos.is_identifier s'
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   115
  | NONE => false);
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   116
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   117
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   118
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   119
(** datatype token **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   121
datatype token_kind =
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   122
  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   123
  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   124
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   125
datatype token = Token of token_kind * string * Position.range;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   126
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   127
fun str_of_token (Token (_, s, _)) = s;
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   128
fun pos_of_token (Token (_, _, (pos, _))) = pos;
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   129
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   130
fun is_proper (Token (Space, _, _)) = false
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   131
  | is_proper (Token (Comment, _, _)) = false
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   132
  | is_proper _ = true;
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   133
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   134
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   135
(* stopper *)
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   136
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   137
fun mk_eof pos = Token (EOF, "", (pos, Position.none));
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   138
val eof = mk_eof Position.none;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   139
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   140
fun is_eof (Token (EOF, _, _)) = true
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   141
  | is_eof _ = false;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   142
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   143
val stopper = Scan.stopper (K eof) is_eof;
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   144
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   146
(* terminal arguments *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   148
val idT = Type ("id", []);
3828
f6a7ca242dc2 added longid;
wenzelm
parents: 2583
diff changeset
   149
val longidT = Type ("longid", []);
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   150
val varT = Type ("var", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   151
val tidT = Type ("tid", []);
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   152
val tvarT = Type ("tvar", []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   154
val terminal_kinds =
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   155
 [("id", IdentSy),
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   156
  ("longid", LongIdentSy),
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   157
  ("var", VarSy),
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   158
  ("tid", TFreeSy),
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   159
  ("tvar", TVarSy),
45703
c7a13ce60161 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
wenzelm
parents: 45666
diff changeset
   160
  ("num_token", NumSy),
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   161
  ("float_token", FloatSy),
45703
c7a13ce60161 renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
wenzelm
parents: 45666
diff changeset
   162
  ("xnum_token", XNumSy),
46483
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
   163
  ("str_token", StrSy)];
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   164
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   165
val terminals = map #1 terminal_kinds;
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20313
diff changeset
   166
val is_terminal = member (op =) terminals;
237
a7d3e712767a MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 164
diff changeset
   167
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   169
(* markup *)
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   170
49821
d15fe10593ff clarified output token markup (see also bc22daeed49e);
wenzelm
parents: 48992
diff changeset
   171
fun literal_markup s =
52189
816c88acd269 more literal tokens, e.g. "EX!";
wenzelm
parents: 51612
diff changeset
   172
  if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter (Symbol.explode s)
816c88acd269 more literal tokens, e.g. "EX!";
wenzelm
parents: 51612
diff changeset
   173
  then Markup.literal
816c88acd269 more literal tokens, e.g. "EX!";
wenzelm
parents: 51612
diff changeset
   174
  else Markup.delimiter;
49821
d15fe10593ff clarified output token markup (see also bc22daeed49e);
wenzelm
parents: 48992
diff changeset
   175
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   176
val token_kind_markup =
51612
6a1e40f9dd55 added var_position in analogy to longid_position, for typing reports on input;
wenzelm
parents: 50242
diff changeset
   177
 fn TFreeSy => Markup.tfree
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   178
  | TVarSy  => Markup.tvar
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   179
  | NumSy   => Markup.numeral
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   180
  | FloatSy => Markup.numeral
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   181
  | XNumSy  => Markup.numeral
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   182
  | StrSy   => Markup.inner_string
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   183
  | Comment => Markup.inner_comment
49821
d15fe10593ff clarified output token markup (see also bc22daeed49e);
wenzelm
parents: 48992
diff changeset
   184
  | _       => Markup.empty;
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   185
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44706
diff changeset
   186
fun report_of_token (Token (kind, s, (pos, _))) =
49821
d15fe10593ff clarified output token markup (see also bc22daeed49e);
wenzelm
parents: 48992
diff changeset
   187
  let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44706
diff changeset
   188
  in (pos, markup) end;
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   189
39510
d9f5f01faa1b Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents: 39507
diff changeset
   190
fun reported_token_range ctxt tok =
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38474
diff changeset
   191
  if is_proper tok
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49821
diff changeset
   192
  then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
39510
d9f5f01faa1b Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm
parents: 39507
diff changeset
   193
  else "";
39168
e3ac771235f7 report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents: 38474
diff changeset
   194
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   195
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   196
(* matching_tokens *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   198
fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   199
  | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k';
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   202
(* valued_token *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   204
fun valued_token (Token (Literal, _, _)) = false
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   205
  | valued_token (Token (EOF, _, _)) = false
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   206
  | valued_token _ = true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   209
(* predef_term *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   211
fun predef_term s =
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   212
  (case AList.lookup (op =) terminal_kinds s of
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   213
    SOME sy => SOME (Token (sy, s, Position.no_range))
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   214
  | NONE => NONE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
46483
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
   217
(* str tokens *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   218
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   219
val scan_chr =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   220
  $$$ "\\" |-- $$$ "'" ||
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   221
  Scan.one
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   222
    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   223
      Symbol_Pos.symbol) >> single ||
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   224
  $$$ "'" --| Scan.ahead (~$$$ "'");
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   225
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   226
val scan_str =
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   227
  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   228
    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   229
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   230
val scan_str_body =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   231
  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   232
    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
14730
59ab60c6fcc6 support nested comments;
wenzelm
parents: 14679
diff changeset
   233
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
46483
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
   235
fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   236
46483
10a9c31a22b4 renamed "xstr" to "str_token";
wenzelm
parents: 45703
diff changeset
   237
fun explode_str str =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   238
  (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   239
    SOME cs => map Symbol_Pos.symbol cs
5868
0022d0a913b5 tuned usage of read;
wenzelm
parents: 5860
diff changeset
   240
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   241
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   242
27806
ece79c0597fe pos_of_token: Position.T;
wenzelm
parents: 27800
diff changeset
   243
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   244
(** tokenize **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   245
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   246
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   247
fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   248
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   249
fun tokenize lex xids syms =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   250
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   251
    val scan_xid =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   252
      if xids then $$$ "_" @@@ scan_id || scan_id
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   253
      else scan_id;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   254
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   255
    val scan_num = scan_hex || scan_bin || scan_int;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   256
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   257
    val scan_val =
26007
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   258
      scan_tvar >> token TVarSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   259
      scan_var >> token VarSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   260
      scan_tid >> token TFreeSy ||
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   261
      scan_float >> token FloatSy ||
26007
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   262
      scan_num >> token NumSy ||
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   263
      $$$ "#" @@@ scan_num >> token XNumSy ||
26007
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   264
      scan_longid >> token LongIdentSy ||
3760d3ff4cce basic scanners: produce symbol list instead of imploded string;
wenzelm
parents: 24630
diff changeset
   265
      scan_xid >> token IdentSy;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   266
27800
df444ddeff56 datatype token: maintain range, tuned representation;
wenzelm
parents: 27773
diff changeset
   267
    val scan_lit = Scan.literal lex >> token Literal;
550
353eea6ec232 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents: 376
diff changeset
   268
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   269
    val scan_token =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   270
      Symbol_Pos.scan_comment !!! >> token Comment ||
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   271
      Scan.max token_leq scan_lit scan_val ||
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   272
      scan_str >> token StrSy ||
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   273
      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   274
  in
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   275
    (case Scan.error
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   276
        (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
27887
9f3fd48cf673 token_kind: add Space, Comment;
wenzelm
parents: 27806
diff changeset
   277
      (toks, []) => toks
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   278
    | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 46483
diff changeset
   279
        Position.here (#1 (Symbol_Pos.range ss))))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   280
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   281
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   282
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   283
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   284
(** scan variables **)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   285
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   286
(* scan_indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   287
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   288
local
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   289
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   290
val scan_vname =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   291
  let
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   292
    fun nat n [] = n
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   293
      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   294
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   295
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   296
    fun chop_idx [] ds = idxname [] ds
50242
56b9c792a98b support for sub-structured identifier syntax (inactive);
wenzelm
parents: 50239
diff changeset
   297
      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
53016
fa9c38891cf2 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents: 52920
diff changeset
   298
      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds  (*legacy*)
fa9c38891cf2 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
wenzelm
parents: 52920
diff changeset
   299
      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds  (*legacy*)
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   300
      | chop_idx (c :: cs) ds =
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   301
          if Symbol.is_digit c then chop_idx cs (c :: ds)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   302
          else idxname (c :: cs) ds;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   303
50239
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   304
    val scan =
fb579401dc26 tuned signature;
wenzelm
parents: 50238
diff changeset
   305
      (scan_id >> map Symbol_Pos.symbol) --
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   306
      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   307
  in
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   308
    scan >>
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   309
      (fn (cs, ~1) => chop_idx (rev cs) []
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   310
        | (cs, i) => (implode cs, i))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   311
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   312
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   313
in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   314
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   315
val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
15443
07f78cc82a73 indexname function now parses type variables as well; changed input
berghofe
parents: 14981
diff changeset
   316
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   317
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   318
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   319
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   320
(* indexname *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   321
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   322
fun read_indexname s =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   323
  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15443
diff changeset
   324
    SOME xi => xi
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   325
  | _ => error ("Lexical error in variable name: " ^ quote s));
18
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
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   328
(* read_var *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   329
4703
a50ab39756db adapted to symbols, scan;
wenzelm
parents: 4587
diff changeset
   330
fun read_var str =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   331
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   332
    val scan =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   333
      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   334
        >> Syntax.var ||
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   335
      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   336
        >> (Syntax.free o implode o map Symbol_Pos.symbol);
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   337
  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   338
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   339
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   340
(* read_variable *)
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   341
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   342
fun read_variable str =
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   343
  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   344
  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
4587
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   345
6bce9ef27d7e added read_var;
wenzelm
parents: 4247
diff changeset
   346
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   347
(* read numbers *)
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   348
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   349
local
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   350
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   351
fun nat cs =
40525
14a2e686bdac eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm
parents: 40290
diff changeset
   352
  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   353
    (Scan.read Symbol_Pos.stopper scan_nat cs);
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   354
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   355
in
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   356
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   357
fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   358
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   359
fun read_int s =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29565
diff changeset
   360
  (case Symbol_Pos.explode (s, Position.none) of
27773
a52166b228b9 improved position handling due to SymbolPos.T;
wenzelm
parents: 27121
diff changeset
   361
    ("-", _) :: cs => Option.map ~ (nat cs)
20313
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   362
  | cs => nat cs);
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   363
bf9101cc4385 renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents: 20165
diff changeset
   364
end;
5860
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   365
ed11c9890852 added read_nat;
wenzelm
parents: 5513
diff changeset
   366
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   367
(* read_xnum: hex/bin/decimal *)
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   368
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   369
local
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   370
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   371
val ten = ord "0" + 10;
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   372
val a = ord "a";
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   373
val A = ord "A";
35428
bd7d6f65976e more systematic mark/unmark operations;
wenzelm
parents: 35262
diff changeset
   374
val _ = a > A orelse raise Fail "Bad ASCII";
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   375
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   376
fun remap_hex c =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   377
  let val x = ord c in
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   378
    if x >= a then chr (x - a + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   379
    else if x >= A then chr (x - A + ten)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   380
    else c
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   381
  end;
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   382
21781
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   383
fun leading_zeros ["0"] = 0
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   384
  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   385
  | leading_zeros _ = 0;
8314ebb5364d read_xnum: return leading_zeros, radix;
wenzelm
parents: 21774
diff changeset
   386
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   387
in
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15570
diff changeset
   388
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   389
fun read_xnum str =
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   390
  let
20096
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   391
    val (sign, radix, digs) =
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   392
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   393
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   394
      | "0" :: "b" :: cs => (1, 2, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   395
      | "-" :: cs => (~1, 10, cs)
7058714024b3 uniform treatment of num/xnum;
wenzelm
parents: 20091
diff changeset
   396
      | cs => (1, 10, cs));
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   397
  in
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   398
   {radix = radix,
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   399
    leading_zeros = leading_zeros digs,
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   400
    value = sign * #1 (Library.read_radix_int radix digs)}
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   401
  end;
9326
1625c1f172b3 added read_xnum;
wenzelm
parents: 9289
diff changeset
   402
15991
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   403
end;
670f8e4b5a98 added read_variable: optional question mark on input;
wenzelm
parents: 15965
diff changeset
   404
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   405
fun read_float str =
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   406
  let
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   407
    val (sign, cs) =
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   408
      (case Symbol.explode str of
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   409
        "-" :: cs => (~1, cs)
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   410
      | cs => (1, cs));
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   411
    val (intpart, fracpart) =
28904
3ef9489eeef5 New lexical item "float".
nipkow
parents: 28413
diff changeset
   412
      (case take_prefix Symbol.is_digit cs of
29156
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   413
        (intpart, "." :: fracpart) => (intpart, fracpart)
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   414
      | _ => raise Fail "read_float");
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   415
  in
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   416
   {mant = sign * #1 (Library.read_int (intpart @ fracpart)),
89f76a58a378 renamed terminal category "float" to "float_token", to avoid name
wenzelm
parents: 28904
diff changeset
   417
    exp = length fracpart}
42046
6341c23baf10 added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents: 40525
diff changeset
   418
  end;
6341c23baf10 added Lexicon.encode_position, Lexicon.decode_position;
wenzelm
parents: 40525
diff changeset
   419
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   420
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   421
(* marked logical entities *)
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   422
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   423
fun marker s = (prefix s, unprefix s);
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   424
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   425
val (mark_class, unmark_class) = marker "\\<^class>";
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   426
val (mark_type, unmark_type) = marker "\\<^type>";
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   427
val (mark_const, unmark_const) = marker "\\<^const>";
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   428
val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   429
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   430
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   431
  (case try unmark_class s of
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   432
    SOME c => case_class c
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   433
  | NONE =>
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   434
      (case try unmark_type s of
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   435
        SOME c => case_type c
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   436
      | NONE =>
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   437
          (case try unmark_const s of
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   438
            SOME c => case_const c
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   439
          | NONE =>
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   440
              (case try unmark_fixed s of
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   441
                SOME c => case_fixed c
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   442
              | NONE => case_default s))));
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   443
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   444
val is_marked =
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   445
  unmark {case_class = K true, case_type = K true, case_const = K true,
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   446
    case_fixed = K true, case_default = K false};
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   447
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   448
val dummy_type = Syntax.const (mark_type "dummy");
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42290
diff changeset
   449
val fun_type = Syntax.const (mark_type "fun");
42290
b1f544c84040 discontinued special treatment of structure Lexicon;
wenzelm
parents: 42264
diff changeset
   450
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
end;