src/Pure/Syntax/lexicon.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50242 56b9c792a98b
child 51612 6a1e40f9dd55
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm@18
     1
(*  Title:      Pure/Syntax/lexicon.ML
wenzelm@18
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     3
wenzelm@4703
     4
Lexer for the inner Isabelle syntax (terms and types).
wenzelm@18
     5
*)
clasohm@0
     6
wenzelm@42290
     7
signature LEXICON =
wenzelm@4247
     8
sig
wenzelm@42476
     9
  structure Syntax:
wenzelm@42476
    10
  sig
wenzelm@42476
    11
    val const: string -> term
wenzelm@42476
    12
    val free: string -> term
wenzelm@42476
    13
    val var: indexname -> term
wenzelm@42476
    14
  end
wenzelm@30573
    15
  val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    16
  val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    17
  val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    18
  val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    19
  val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@40290
    20
  val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    21
  val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    22
  val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    23
  val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@30573
    24
  val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
wenzelm@50239
    25
  val is_tid: string -> bool
wenzelm@27800
    26
  datatype token_kind =
wenzelm@27887
    27
    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
nipkow@28904
    28
    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
wenzelm@27800
    29
  datatype token = Token of token_kind * string * Position.range
wenzelm@27806
    30
  val str_of_token: token -> string
wenzelm@27806
    31
  val pos_of_token: token -> Position.T
wenzelm@27887
    32
  val is_proper: token -> bool
wenzelm@27800
    33
  val mk_eof: Position.T -> token
wenzelm@27800
    34
  val eof: token
wenzelm@27800
    35
  val is_eof: token -> bool
wenzelm@27800
    36
  val stopper: token Scan.stopper
wenzelm@550
    37
  val idT: typ
wenzelm@3828
    38
  val longidT: typ
wenzelm@550
    39
  val varT: typ
wenzelm@550
    40
  val tidT: typ
wenzelm@550
    41
  val tvarT: typ
wenzelm@237
    42
  val terminals: string list
wenzelm@237
    43
  val is_terminal: string -> bool
wenzelm@49821
    44
  val literal_markup: string -> Markup.T
wenzelm@44736
    45
  val report_of_token: token -> Position.report
wenzelm@39510
    46
  val reported_token_range: Proof.context -> token -> string
wenzelm@18
    47
  val matching_tokens: token * token -> bool
wenzelm@18
    48
  val valued_token: token -> bool
wenzelm@237
    49
  val predef_term: string -> token option
wenzelm@46483
    50
  val implode_str: string list -> string
wenzelm@46483
    51
  val explode_str: string -> string list
wenzelm@30573
    52
  val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
wenzelm@42290
    53
  val read_indexname: string -> indexname
wenzelm@42290
    54
  val read_var: string -> term
wenzelm@42290
    55
  val read_variable: string -> indexname option
wenzelm@42290
    56
  val read_nat: string -> int option
wenzelm@42290
    57
  val read_int: string -> int option
wenzelm@42290
    58
  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
wenzelm@42290
    59
  val read_float: string -> {mant: int, exp: int}
wenzelm@42290
    60
  val mark_class: string -> string val unmark_class: string -> string
wenzelm@42290
    61
  val mark_type: string -> string val unmark_type: string -> string
wenzelm@42290
    62
  val mark_const: string -> string val unmark_const: string -> string
wenzelm@42290
    63
  val mark_fixed: string -> string val unmark_fixed: string -> string
wenzelm@42290
    64
  val unmark:
wenzelm@42290
    65
   {case_class: string -> 'a,
wenzelm@42290
    66
    case_type: string -> 'a,
wenzelm@42290
    67
    case_const: string -> 'a,
wenzelm@42290
    68
    case_fixed: string -> 'a,
wenzelm@42290
    69
    case_default: string -> 'a} -> string -> 'a
wenzelm@42290
    70
  val is_marked: string -> bool
wenzelm@42290
    71
  val dummy_type: term
wenzelm@42290
    72
  val fun_type: term
wenzelm@4247
    73
end;
clasohm@0
    74
wenzelm@14679
    75
structure Lexicon: LEXICON =
clasohm@0
    76
struct
clasohm@0
    77
wenzelm@42476
    78
(** syntaxtic terms **)
wenzelm@42476
    79
wenzelm@42476
    80
structure Syntax =
wenzelm@42476
    81
struct
wenzelm@42476
    82
wenzelm@42476
    83
fun const c = Const (c, dummyT);
wenzelm@42476
    84
fun free x = Free (x, dummyT);
wenzelm@42476
    85
fun var xi = Var (xi, dummyT);
wenzelm@42476
    86
wenzelm@42476
    87
end;
wenzelm@42476
    88
wenzelm@42476
    89
wenzelm@42476
    90
wenzelm@4703
    91
(** basic scanners **)
wenzelm@4703
    92
wenzelm@30573
    93
open Basic_Symbol_Pos;
wenzelm@27773
    94
wenzelm@43947
    95
fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
wenzelm@27773
    96
wenzelm@50239
    97
val scan_id = Symbol_Pos.scan_ident;
wenzelm@27773
    98
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
wenzelm@27773
    99
val scan_tid = $$$ "'" @@@ scan_id;
wenzelm@4703
   100
wenzelm@40525
   101
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
wenzelm@27773
   102
val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
nipkow@28904
   103
val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
nipkow@28904
   104
val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
wenzelm@40525
   105
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
wenzelm@27773
   106
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
wenzelm@4703
   107
wenzelm@27773
   108
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
wenzelm@27773
   109
val scan_var = $$$ "?" @@@ scan_id_nat;
wenzelm@27773
   110
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
wenzelm@4703
   111
wenzelm@50239
   112
fun is_tid s =
wenzelm@50239
   113
  (case try (unprefix "'") s of
wenzelm@50239
   114
    SOME s' => Symbol_Pos.is_identifier s'
wenzelm@50239
   115
  | NONE => false);
wenzelm@50239
   116
wenzelm@4703
   117
wenzelm@4703
   118
wenzelm@18
   119
(** datatype token **)
clasohm@0
   120
wenzelm@27800
   121
datatype token_kind =
wenzelm@27887
   122
  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
nipkow@28904
   123
  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
wenzelm@27800
   124
wenzelm@27800
   125
datatype token = Token of token_kind * string * Position.range;
wenzelm@27800
   126
wenzelm@27806
   127
fun str_of_token (Token (_, s, _)) = s;
wenzelm@27806
   128
fun pos_of_token (Token (_, _, (pos, _))) = pos;
wenzelm@27806
   129
wenzelm@27887
   130
fun is_proper (Token (Space, _, _)) = false
wenzelm@27887
   131
  | is_proper (Token (Comment, _, _)) = false
wenzelm@27887
   132
  | is_proper _ = true;
wenzelm@27887
   133
wenzelm@27800
   134
wenzelm@27800
   135
(* stopper *)
wenzelm@27800
   136
wenzelm@27800
   137
fun mk_eof pos = Token (EOF, "", (pos, Position.none));
wenzelm@27800
   138
val eof = mk_eof Position.none;
wenzelm@27800
   139
wenzelm@27800
   140
fun is_eof (Token (EOF, _, _)) = true
wenzelm@27800
   141
  | is_eof _ = false;
wenzelm@27800
   142
wenzelm@27800
   143
val stopper = Scan.stopper (K eof) is_eof;
wenzelm@27800
   144
clasohm@0
   145
wenzelm@237
   146
(* terminal arguments *)
clasohm@0
   147
wenzelm@550
   148
val idT = Type ("id", []);
wenzelm@3828
   149
val longidT = Type ("longid", []);
wenzelm@550
   150
val varT = Type ("var", []);
wenzelm@550
   151
val tidT = Type ("tid", []);
wenzelm@550
   152
val tvarT = Type ("tvar", []);
clasohm@0
   153
wenzelm@29156
   154
val terminal_kinds =
wenzelm@29156
   155
 [("id", IdentSy),
wenzelm@29156
   156
  ("longid", LongIdentSy),
wenzelm@29156
   157
  ("var", VarSy),
wenzelm@29156
   158
  ("tid", TFreeSy),
wenzelm@29156
   159
  ("tvar", TVarSy),
wenzelm@45703
   160
  ("num_token", NumSy),
wenzelm@29156
   161
  ("float_token", FloatSy),
wenzelm@45703
   162
  ("xnum_token", XNumSy),
wenzelm@46483
   163
  ("str_token", StrSy)];
wenzelm@29156
   164
wenzelm@29156
   165
val terminals = map #1 terminal_kinds;
wenzelm@20664
   166
val is_terminal = member (op =) terminals;
wenzelm@237
   167
clasohm@0
   168
wenzelm@27887
   169
(* markup *)
wenzelm@27887
   170
wenzelm@49821
   171
fun literal_markup s =
wenzelm@50238
   172
  if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
wenzelm@49821
   173
wenzelm@27887
   174
val token_kind_markup =
wenzelm@50201
   175
 fn VarSy   => Markup.var
wenzelm@50201
   176
  | TFreeSy => Markup.tfree
wenzelm@50201
   177
  | TVarSy  => Markup.tvar
wenzelm@50201
   178
  | NumSy   => Markup.numeral
wenzelm@50201
   179
  | FloatSy => Markup.numeral
wenzelm@50201
   180
  | XNumSy  => Markup.numeral
wenzelm@50201
   181
  | StrSy   => Markup.inner_string
wenzelm@50201
   182
  | Comment => Markup.inner_comment
wenzelm@49821
   183
  | _       => Markup.empty;
wenzelm@27887
   184
wenzelm@44736
   185
fun report_of_token (Token (kind, s, (pos, _))) =
wenzelm@49821
   186
  let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
wenzelm@44736
   187
  in (pos, markup) end;
wenzelm@27887
   188
wenzelm@39510
   189
fun reported_token_range ctxt tok =
wenzelm@39168
   190
  if is_proper tok
wenzelm@50201
   191
  then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
wenzelm@39510
   192
  else "";
wenzelm@39168
   193
wenzelm@27887
   194
wenzelm@18
   195
(* matching_tokens *)
clasohm@0
   196
wenzelm@27800
   197
fun matching_tokens (Token (Literal, x, _), Token (Literal, y, _)) = x = y
wenzelm@27800
   198
  | matching_tokens (Token (k, _, _), Token (k', _, _)) = k = k';
clasohm@0
   199
clasohm@0
   200
wenzelm@18
   201
(* valued_token *)
clasohm@0
   202
wenzelm@27800
   203
fun valued_token (Token (Literal, _, _)) = false
wenzelm@27800
   204
  | valued_token (Token (EOF, _, _)) = false
wenzelm@27800
   205
  | valued_token _ = true;
clasohm@0
   206
clasohm@0
   207
wenzelm@18
   208
(* predef_term *)
clasohm@0
   209
wenzelm@29156
   210
fun predef_term s =
wenzelm@29156
   211
  (case AList.lookup (op =) terminal_kinds s of
wenzelm@29156
   212
    SOME sy => SOME (Token (sy, s, Position.no_range))
wenzelm@29156
   213
  | NONE => NONE);
clasohm@0
   214
clasohm@0
   215
wenzelm@46483
   216
(* str tokens *)
wenzelm@18
   217
wenzelm@14730
   218
val scan_chr =
wenzelm@27773
   219
  $$$ "\\" |-- $$$ "'" ||
wenzelm@40525
   220
  Scan.one
wenzelm@40525
   221
    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
wenzelm@40525
   222
      Symbol_Pos.symbol) >> single ||
wenzelm@27773
   223
  $$$ "'" --| Scan.ahead (~$$$ "'");
wenzelm@14730
   224
wenzelm@14730
   225
val scan_str =
wenzelm@27800
   226
  $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
wenzelm@27800
   227
    ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
wenzelm@27800
   228
wenzelm@27800
   229
val scan_str_body =
wenzelm@27773
   230
  $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
wenzelm@27773
   231
    ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
wenzelm@14730
   232
clasohm@0
   233
wenzelm@46483
   234
fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
wenzelm@18
   235
wenzelm@46483
   236
fun explode_str str =
wenzelm@30573
   237
  (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
wenzelm@40525
   238
    SOME cs => map Symbol_Pos.symbol cs
wenzelm@5868
   239
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
wenzelm@18
   240
wenzelm@18
   241
wenzelm@27806
   242
wenzelm@18
   243
(** tokenize **)
wenzelm@18
   244
wenzelm@27800
   245
fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
wenzelm@30573
   246
fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
wenzelm@27800
   247
wenzelm@27800
   248
fun tokenize lex xids syms =
wenzelm@18
   249
  let
wenzelm@18
   250
    val scan_xid =
wenzelm@27773
   251
      if xids then $$$ "_" @@@ scan_id || scan_id
wenzelm@18
   252
      else scan_id;
wenzelm@18
   253
wenzelm@20096
   254
    val scan_num = scan_hex || scan_bin || scan_int;
wenzelm@20096
   255
wenzelm@550
   256
    val scan_val =
wenzelm@26007
   257
      scan_tvar >> token TVarSy ||
wenzelm@26007
   258
      scan_var >> token VarSy ||
wenzelm@26007
   259
      scan_tid >> token TFreeSy ||
nipkow@28904
   260
      scan_float >> token FloatSy ||
wenzelm@26007
   261
      scan_num >> token NumSy ||
wenzelm@27773
   262
      $$$ "#" @@@ scan_num >> token XNumSy ||
wenzelm@26007
   263
      scan_longid >> token LongIdentSy ||
wenzelm@26007
   264
      scan_xid >> token IdentSy;
wenzelm@18
   265
wenzelm@27800
   266
    val scan_lit = Scan.literal lex >> token Literal;
wenzelm@550
   267
wenzelm@4703
   268
    val scan_token =
wenzelm@30573
   269
      Symbol_Pos.scan_comment !!! >> token Comment ||
wenzelm@27887
   270
      Scan.max token_leq scan_lit scan_val ||
wenzelm@27887
   271
      scan_str >> token StrSy ||
wenzelm@40525
   272
      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
wenzelm@18
   273
  in
wenzelm@27773
   274
    (case Scan.error
wenzelm@30573
   275
        (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
wenzelm@27887
   276
      (toks, []) => toks
wenzelm@30573
   277
    | (_, ss) => error ("Inner lexical error at: " ^ Symbol_Pos.content ss ^
wenzelm@48992
   278
        Position.here (#1 (Symbol_Pos.range ss))))
wenzelm@18
   279
  end;
wenzelm@18
   280
wenzelm@18
   281
wenzelm@18
   282
wenzelm@18
   283
(** scan variables **)
wenzelm@18
   284
wenzelm@15991
   285
(* scan_indexname *)
wenzelm@15991
   286
wenzelm@15991
   287
local
wenzelm@18
   288
wenzelm@27773
   289
val scan_vname =
wenzelm@18
   290
  let
wenzelm@15991
   291
    fun nat n [] = n
wenzelm@15991
   292
      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
wenzelm@18
   293
wenzelm@15991
   294
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
wenzelm@15991
   295
    fun chop_idx [] ds = idxname [] ds
wenzelm@50242
   296
      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
wenzelm@15991
   297
      | chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
wenzelm@15991
   298
      | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
wenzelm@15991
   299
      | chop_idx (c :: cs) ds =
wenzelm@15991
   300
          if Symbol.is_digit c then chop_idx cs (c :: ds)
wenzelm@15991
   301
          else idxname (c :: cs) ds;
wenzelm@18
   302
wenzelm@50239
   303
    val scan =
wenzelm@50239
   304
      (scan_id >> map Symbol_Pos.symbol) --
wenzelm@40525
   305
      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
wenzelm@18
   306
  in
wenzelm@27773
   307
    scan >>
wenzelm@27773
   308
      (fn (cs, ~1) => chop_idx (rev cs) []
wenzelm@27773
   309
        | (cs, i) => (implode cs, i))
wenzelm@18
   310
  end;
wenzelm@18
   311
wenzelm@15991
   312
in
wenzelm@18
   313
wenzelm@27773
   314
val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
berghofe@15443
   315
wenzelm@15991
   316
end;
wenzelm@15991
   317
wenzelm@15991
   318
wenzelm@15991
   319
(* indexname *)
wenzelm@15991
   320
wenzelm@20313
   321
fun read_indexname s =
wenzelm@30573
   322
  (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
skalberg@15531
   323
    SOME xi => xi
wenzelm@20313
   324
  | _ => error ("Lexical error in variable name: " ^ quote s));
wenzelm@18
   325
wenzelm@18
   326
wenzelm@4703
   327
(* read_var *)
wenzelm@18
   328
wenzelm@4703
   329
fun read_var str =
wenzelm@18
   330
  let
wenzelm@18
   331
    val scan =
wenzelm@42476
   332
      $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
wenzelm@42476
   333
        >> Syntax.var ||
wenzelm@42476
   334
      Scan.many (Symbol.is_regular o Symbol_Pos.symbol)
wenzelm@42476
   335
        >> (Syntax.free o implode o map Symbol_Pos.symbol);
wenzelm@30573
   336
  in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
wenzelm@15991
   337
wenzelm@15991
   338
wenzelm@15991
   339
(* read_variable *)
wenzelm@15991
   340
wenzelm@15991
   341
fun read_variable str =
wenzelm@27773
   342
  let val scan = $$$ "?" |-- scan_indexname || scan_indexname
wenzelm@30573
   343
  in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
wenzelm@4587
   344
wenzelm@4587
   345
wenzelm@20313
   346
(* read numbers *)
wenzelm@20313
   347
wenzelm@20313
   348
local
wenzelm@20313
   349
wenzelm@20313
   350
fun nat cs =
wenzelm@40525
   351
  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
wenzelm@30573
   352
    (Scan.read Symbol_Pos.stopper scan_nat cs);
wenzelm@5860
   353
wenzelm@20313
   354
in
wenzelm@20313
   355
wenzelm@30573
   356
fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
wenzelm@20313
   357
wenzelm@20313
   358
fun read_int s =
wenzelm@30573
   359
  (case Symbol_Pos.explode (s, Position.none) of
wenzelm@27773
   360
    ("-", _) :: cs => Option.map ~ (nat cs)
wenzelm@20313
   361
  | cs => nat cs);
wenzelm@20313
   362
wenzelm@20313
   363
end;
wenzelm@5860
   364
wenzelm@5860
   365
wenzelm@20096
   366
(* read_xnum: hex/bin/decimal *)
wenzelm@9326
   367
wenzelm@15991
   368
local
wenzelm@15991
   369
wenzelm@20096
   370
val ten = ord "0" + 10;
wenzelm@20096
   371
val a = ord "a";
wenzelm@20096
   372
val A = ord "A";
wenzelm@35428
   373
val _ = a > A orelse raise Fail "Bad ASCII";
wenzelm@20096
   374
wenzelm@20096
   375
fun remap_hex c =
wenzelm@20096
   376
  let val x = ord c in
wenzelm@20096
   377
    if x >= a then chr (x - a + ten)
wenzelm@20096
   378
    else if x >= A then chr (x - A + ten)
wenzelm@20096
   379
    else c
wenzelm@20096
   380
  end;
wenzelm@15991
   381
wenzelm@21781
   382
fun leading_zeros ["0"] = 0
wenzelm@21781
   383
  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
wenzelm@21781
   384
  | leading_zeros _ = 0;
wenzelm@21781
   385
wenzelm@15991
   386
in
paulson@15965
   387
wenzelm@9326
   388
fun read_xnum str =
wenzelm@9326
   389
  let
wenzelm@20096
   390
    val (sign, radix, digs) =
wenzelm@20096
   391
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
wenzelm@20096
   392
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
wenzelm@20096
   393
      | "0" :: "b" :: cs => (1, 2, cs)
wenzelm@20096
   394
      | "-" :: cs => (~1, 10, cs)
wenzelm@20096
   395
      | cs => (1, 10, cs));
wenzelm@29156
   396
  in
wenzelm@29156
   397
   {radix = radix,
wenzelm@29156
   398
    leading_zeros = leading_zeros digs,
wenzelm@29156
   399
    value = sign * #1 (Library.read_radix_int radix digs)}
wenzelm@29156
   400
  end;
wenzelm@9326
   401
wenzelm@15991
   402
end;
wenzelm@15991
   403
nipkow@28904
   404
fun read_float str =
nipkow@28904
   405
  let
nipkow@28904
   406
    val (sign, cs) =
wenzelm@29156
   407
      (case Symbol.explode str of
wenzelm@29156
   408
        "-" :: cs => (~1, cs)
wenzelm@29156
   409
      | cs => (1, cs));
wenzelm@29156
   410
    val (intpart, fracpart) =
nipkow@28904
   411
      (case take_prefix Symbol.is_digit cs of
wenzelm@29156
   412
        (intpart, "." :: fracpart) => (intpart, fracpart)
wenzelm@29156
   413
      | _ => raise Fail "read_float");
wenzelm@29156
   414
  in
wenzelm@29156
   415
   {mant = sign * #1 (Library.read_int (intpart @ fracpart)),
wenzelm@29156
   416
    exp = length fracpart}
wenzelm@42046
   417
  end;
wenzelm@42046
   418
wenzelm@42290
   419
wenzelm@42290
   420
(* marked logical entities *)
wenzelm@42290
   421
wenzelm@42290
   422
fun marker s = (prefix s, unprefix s);
wenzelm@42290
   423
wenzelm@42290
   424
val (mark_class, unmark_class) = marker "\\<^class>";
wenzelm@42290
   425
val (mark_type, unmark_type) = marker "\\<^type>";
wenzelm@42290
   426
val (mark_const, unmark_const) = marker "\\<^const>";
wenzelm@42290
   427
val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
wenzelm@42290
   428
wenzelm@42290
   429
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
wenzelm@42290
   430
  (case try unmark_class s of
wenzelm@42290
   431
    SOME c => case_class c
wenzelm@42290
   432
  | NONE =>
wenzelm@42290
   433
      (case try unmark_type s of
wenzelm@42290
   434
        SOME c => case_type c
wenzelm@42290
   435
      | NONE =>
wenzelm@42290
   436
          (case try unmark_const s of
wenzelm@42290
   437
            SOME c => case_const c
wenzelm@42290
   438
          | NONE =>
wenzelm@42290
   439
              (case try unmark_fixed s of
wenzelm@42290
   440
                SOME c => case_fixed c
wenzelm@42290
   441
              | NONE => case_default s))));
wenzelm@42290
   442
wenzelm@42290
   443
val is_marked =
wenzelm@42290
   444
  unmark {case_class = K true, case_type = K true, case_const = K true,
wenzelm@42290
   445
    case_fixed = K true, case_default = K false};
wenzelm@42290
   446
wenzelm@42476
   447
val dummy_type = Syntax.const (mark_type "dummy");
wenzelm@42476
   448
val fun_type = Syntax.const (mark_type "fun");
wenzelm@42290
   449
clasohm@0
   450
end;