src/Pure/Syntax/lexicon.ML
author wenzelm
Thu Aug 30 15:04:42 2007 +0200 (2007-08-30 ago)
changeset 24484 013b98b57b86
parent 24245 4ffeb1dd048a
child 24583 d77e4d48e497
permissions -rw-r--r--
maintain mode in context (get/set/restore_mode);
wenzelm@18
     1
(*  Title:      Pure/Syntax/lexicon.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@18
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
wenzelm@4703
     5
Lexer for the inner Isabelle syntax (terms and types).
wenzelm@18
     6
*)
clasohm@0
     7
clasohm@0
     8
signature LEXICON0 =
wenzelm@4247
     9
sig
clasohm@0
    10
  val is_identifier: string -> bool
wenzelm@14679
    11
  val is_ascii_identifier: string -> bool
wenzelm@20165
    12
  val is_tid: string -> bool
wenzelm@4247
    13
  val implode_xstr: string list -> string
wenzelm@4247
    14
  val explode_xstr: string -> string list
wenzelm@4703
    15
  val scan_id: string list -> string * string list
wenzelm@4703
    16
  val scan_longid: string list -> string * string list
wenzelm@4703
    17
  val scan_var: string list -> string * string list
wenzelm@4703
    18
  val scan_tid: string list -> string * string list
wenzelm@4902
    19
  val scan_tvar: string list -> string * string list
wenzelm@4703
    20
  val scan_nat: string list -> string * string list
wenzelm@4703
    21
  val scan_int: string list -> string * string list
kleing@20067
    22
  val scan_hex: string list -> string * string list
kleing@20067
    23
  val scan_bin: string list -> string * string list
wenzelm@20313
    24
  val read_indexname: string -> indexname
wenzelm@4703
    25
  val read_var: string -> term
wenzelm@15991
    26
  val read_variable: string -> indexname option
wenzelm@550
    27
  val const: string -> term
wenzelm@550
    28
  val free: string -> term
wenzelm@550
    29
  val var: indexname -> term
wenzelm@5860
    30
  val read_nat: string -> int option
wenzelm@20313
    31
  val read_int: string -> int option
wenzelm@21781
    32
  val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int}
wenzelm@7784
    33
  val read_idents: string -> string list
wenzelm@19002
    34
  val fixedN: string
wenzelm@19002
    35
  val constN: string
wenzelm@4247
    36
end;
clasohm@0
    37
clasohm@0
    38
signature LEXICON =
wenzelm@4247
    39
sig
wenzelm@18
    40
  include LEXICON0
wenzelm@18
    41
  val is_xid: string -> bool
wenzelm@18
    42
  datatype token =
wenzelm@18
    43
    Token of string |
wenzelm@18
    44
    IdentSy of string |
wenzelm@3828
    45
    LongIdentSy of string |
wenzelm@18
    46
    VarSy of string |
wenzelm@18
    47
    TFreeSy of string |
wenzelm@18
    48
    TVarSy of string |
wenzelm@550
    49
    NumSy of string |
wenzelm@11697
    50
    XNumSy of string |
wenzelm@550
    51
    StrSy of string |
wenzelm@237
    52
    EndToken
wenzelm@550
    53
  val idT: typ
wenzelm@3828
    54
  val longidT: typ
wenzelm@550
    55
  val varT: typ
wenzelm@550
    56
  val tidT: typ
wenzelm@550
    57
  val tvarT: typ
wenzelm@237
    58
  val terminals: string list
wenzelm@237
    59
  val is_terminal: string -> bool
wenzelm@18
    60
  val str_of_token: token -> string
wenzelm@18
    61
  val display_token: token -> string
wenzelm@18
    62
  val matching_tokens: token * token -> bool
wenzelm@18
    63
  val valued_token: token -> bool
wenzelm@237
    64
  val predef_term: string -> token option
wenzelm@4703
    65
  val tokenize: Scan.lexicon -> bool -> string list -> token list
wenzelm@4247
    66
end;
clasohm@0
    67
wenzelm@14679
    68
structure Lexicon: LEXICON =
clasohm@0
    69
struct
clasohm@0
    70
wenzelm@4247
    71
wenzelm@18
    72
(** is_identifier etc. **)
wenzelm@18
    73
wenzelm@16150
    74
val is_identifier = Symbol.is_ident o Symbol.explode;
wenzelm@18
    75
wenzelm@14679
    76
fun is_ascii_identifier s =
wenzelm@14679
    77
  let val cs = Symbol.explode s
wenzelm@16150
    78
  in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end;
wenzelm@14679
    79
wenzelm@18
    80
fun is_xid s =
wenzelm@4703
    81
  (case Symbol.explode s of
wenzelm@16150
    82
    "_" :: cs => Symbol.is_ident cs
wenzelm@16150
    83
  | cs => Symbol.is_ident cs);
wenzelm@18
    84
clasohm@330
    85
fun is_tid s =
wenzelm@4703
    86
  (case Symbol.explode s of
wenzelm@16150
    87
    "'" :: cs => Symbol.is_ident cs
wenzelm@18
    88
  | _ => false);
wenzelm@18
    89
clasohm@0
    90
clasohm@0
    91
wenzelm@4703
    92
(** basic scanners **)
wenzelm@4703
    93
wenzelm@21858
    94
val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.many Symbol.is_letdig >> op ::;
wenzelm@21858
    95
val scan_digits1 = Scan.many1 Symbol.is_digit;
wenzelm@21858
    96
val scan_hex1 = Scan.many1 (Symbol.is_digit orf Symbol.is_hex_letter);
wenzelm@21858
    97
val scan_bin1 = Scan.many1 (fn s => s = "0" orelse s = "1");
wenzelm@4703
    98
wenzelm@4703
    99
val scan_id = scan_letter_letdigs >> implode;
wenzelm@4703
   100
val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
wenzelm@4703
   101
val scan_tid = $$ "'" ^^ scan_id;
wenzelm@4703
   102
wenzelm@4703
   103
val scan_nat = scan_digits1 >> implode;
paulson@5513
   104
val scan_int = $$ "-" ^^ scan_nat || scan_nat;
wenzelm@4703
   105
wenzelm@20091
   106
val scan_hex = $$ "0" ^^ $$ "x" ^^ (scan_hex1 >> implode);
wenzelm@20091
   107
val scan_bin = $$ "0" ^^ $$ "b" ^^ (scan_bin1 >> implode);
kleing@20067
   108
wenzelm@4703
   109
val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
wenzelm@4703
   110
val scan_var = $$ "?" ^^ scan_id_nat;
wenzelm@4902
   111
val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
wenzelm@4703
   112
wenzelm@4703
   113
wenzelm@4703
   114
wenzelm@18
   115
(** datatype token **)
clasohm@0
   116
wenzelm@18
   117
datatype token =
wenzelm@18
   118
  Token of string |
wenzelm@18
   119
  IdentSy of string |
wenzelm@3828
   120
  LongIdentSy of string |
wenzelm@18
   121
  VarSy of string |
wenzelm@18
   122
  TFreeSy of string |
wenzelm@18
   123
  TVarSy of string |
wenzelm@550
   124
  NumSy of string |
wenzelm@11697
   125
  XNumSy of string |
wenzelm@550
   126
  StrSy of string |
wenzelm@18
   127
  EndToken;
clasohm@0
   128
clasohm@0
   129
wenzelm@237
   130
(* terminal arguments *)
clasohm@0
   131
wenzelm@550
   132
val idT = Type ("id", []);
wenzelm@3828
   133
val longidT = Type ("longid", []);
wenzelm@550
   134
val varT = Type ("var", []);
wenzelm@550
   135
val tidT = Type ("tid", []);
wenzelm@550
   136
val tvarT = Type ("tvar", []);
clasohm@0
   137
wenzelm@11697
   138
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
wenzelm@20664
   139
val is_terminal = member (op =) terminals;
wenzelm@237
   140
clasohm@0
   141
wenzelm@18
   142
(* str_of_token *)
clasohm@0
   143
wenzelm@18
   144
fun str_of_token (Token s) = s
wenzelm@18
   145
  | str_of_token (IdentSy s) = s
wenzelm@3828
   146
  | str_of_token (LongIdentSy s) = s
wenzelm@18
   147
  | str_of_token (VarSy s) = s
wenzelm@18
   148
  | str_of_token (TFreeSy s) = s
wenzelm@18
   149
  | str_of_token (TVarSy s) = s
wenzelm@550
   150
  | str_of_token (NumSy s) = s
wenzelm@11697
   151
  | str_of_token (XNumSy s) = s
wenzelm@550
   152
  | str_of_token (StrSy s) = s
wenzelm@376
   153
  | str_of_token EndToken = "EOF";
clasohm@0
   154
wenzelm@18
   155
wenzelm@18
   156
(* display_token *)
clasohm@0
   157
wenzelm@18
   158
fun display_token (Token s) = quote s
wenzelm@18
   159
  | display_token (IdentSy s) = "id(" ^ s ^ ")"
wenzelm@3828
   160
  | display_token (LongIdentSy s) = "longid(" ^ s ^ ")"
wenzelm@18
   161
  | display_token (VarSy s) = "var(" ^ s ^ ")"
clasohm@330
   162
  | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
wenzelm@18
   163
  | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
wenzelm@11697
   164
  | display_token (NumSy s) = "num(" ^ s ^ ")"
wenzelm@11697
   165
  | display_token (XNumSy s) = "xnum(" ^ s ^ ")"
wenzelm@550
   166
  | display_token (StrSy s) = "xstr(" ^ s ^ ")"
wenzelm@18
   167
  | display_token EndToken = "";
clasohm@0
   168
wenzelm@18
   169
wenzelm@18
   170
(* matching_tokens *)
clasohm@0
   171
wenzelm@18
   172
fun matching_tokens (Token x, Token y) = (x = y)
wenzelm@18
   173
  | matching_tokens (IdentSy _, IdentSy _) = true
wenzelm@3828
   174
  | matching_tokens (LongIdentSy _, LongIdentSy _) = true
wenzelm@18
   175
  | matching_tokens (VarSy _, VarSy _) = true
wenzelm@18
   176
  | matching_tokens (TFreeSy _, TFreeSy _) = true
wenzelm@18
   177
  | matching_tokens (TVarSy _, TVarSy _) = true
wenzelm@550
   178
  | matching_tokens (NumSy _, NumSy _) = true
wenzelm@11697
   179
  | matching_tokens (XNumSy _, XNumSy _) = true
wenzelm@550
   180
  | matching_tokens (StrSy _, StrSy _) = true
wenzelm@18
   181
  | matching_tokens (EndToken, EndToken) = true
wenzelm@18
   182
  | matching_tokens _ = false;
clasohm@0
   183
clasohm@0
   184
wenzelm@18
   185
(* valued_token *)
clasohm@0
   186
wenzelm@18
   187
fun valued_token (Token _) = false
wenzelm@18
   188
  | valued_token (IdentSy _) = true
wenzelm@3828
   189
  | valued_token (LongIdentSy _) = true
wenzelm@18
   190
  | valued_token (VarSy _) = true
wenzelm@18
   191
  | valued_token (TFreeSy _) = true
wenzelm@18
   192
  | valued_token (TVarSy _) = true
wenzelm@550
   193
  | valued_token (NumSy _) = true
wenzelm@11697
   194
  | valued_token (XNumSy _) = true
wenzelm@550
   195
  | valued_token (StrSy _) = true
wenzelm@18
   196
  | valued_token EndToken = false;
clasohm@0
   197
clasohm@0
   198
wenzelm@18
   199
(* predef_term *)
clasohm@0
   200
skalberg@15531
   201
fun predef_term "id" = SOME (IdentSy "id")
skalberg@15531
   202
  | predef_term "longid" = SOME (LongIdentSy "longid")
skalberg@15531
   203
  | predef_term "var" = SOME (VarSy "var")
skalberg@15531
   204
  | predef_term "tid" = SOME (TFreeSy "tid")
skalberg@15531
   205
  | predef_term "tvar" = SOME (TVarSy "tvar")
skalberg@15531
   206
  | predef_term "num" = SOME (NumSy "num")
skalberg@15531
   207
  | predef_term "xnum" = SOME (XNumSy "xnum")
skalberg@15531
   208
  | predef_term "xstr" = SOME (StrSy "xstr")
skalberg@15531
   209
  | predef_term _ = NONE;
clasohm@0
   210
clasohm@0
   211
wenzelm@4703
   212
(* xstr tokens *)
wenzelm@18
   213
wenzelm@14730
   214
fun lex_err msg prfx (cs, _) =
wenzelm@14730
   215
  "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs);
wenzelm@14730
   216
wenzelm@14730
   217
val scan_chr =
wenzelm@21774
   218
  $$ "\\" |-- $$ "'" ||
wenzelm@23784
   219
  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) ||
wenzelm@19305
   220
  $$ "'" --| Scan.ahead (~$$ "'");
wenzelm@14730
   221
wenzelm@14730
   222
val scan_str =
wenzelm@14730
   223
  $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''")
wenzelm@14730
   224
    (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
wenzelm@14730
   225
clasohm@0
   226
wenzelm@4703
   227
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
wenzelm@18
   228
wenzelm@4703
   229
fun explode_xstr str =
wenzelm@5868
   230
  (case Scan.read Symbol.stopper scan_str (Symbol.explode str) of
skalberg@15531
   231
    SOME cs => cs
wenzelm@5868
   232
  | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
wenzelm@18
   233
wenzelm@18
   234
wenzelm@14730
   235
(* nested comments *)
wenzelm@14730
   236
wenzelm@14730
   237
val scan_cmt =
wenzelm@14730
   238
  Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
wenzelm@14730
   239
  Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
wenzelm@19305
   240
  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
wenzelm@23784
   241
  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
wenzelm@14730
   242
wenzelm@14783
   243
val scan_comment =
wenzelm@14783
   244
  $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
wenzelm@14730
   245
    (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")")
wenzelm@14783
   246
  >> K ();
wenzelm@14730
   247
wenzelm@14730
   248
wenzelm@18
   249
wenzelm@18
   250
(** tokenize **)
wenzelm@18
   251
wenzelm@2363
   252
fun tokenize lex xids chs =
wenzelm@18
   253
  let
wenzelm@18
   254
    val scan_xid =
wenzelm@18
   255
      if xids then $$ "_" ^^ scan_id || scan_id
wenzelm@18
   256
      else scan_id;
wenzelm@18
   257
wenzelm@20096
   258
    val scan_num = scan_hex || scan_bin || scan_int;
wenzelm@20096
   259
wenzelm@550
   260
    val scan_val =
wenzelm@4902
   261
      scan_tvar >> pair TVarSy ||
wenzelm@4703
   262
      scan_var >> pair VarSy ||
wenzelm@4703
   263
      scan_tid >> pair TFreeSy ||
wenzelm@20096
   264
      scan_num >> pair NumSy ||
wenzelm@20096
   265
      $$ "#" ^^ scan_num >> pair XNumSy ||
wenzelm@3828
   266
      scan_longid >> pair LongIdentSy ||
wenzelm@18
   267
      scan_xid >> pair IdentSy;
wenzelm@18
   268
wenzelm@4703
   269
    val scan_lit = Scan.literal lex >> (pair Token o implode);
wenzelm@550
   270
wenzelm@4703
   271
    val scan_token =
skalberg@15531
   272
      scan_comment >> K NONE ||
skalberg@15531
   273
      Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => SOME (tk s)) ||
skalberg@15531
   274
      scan_str >> (SOME o StrSy o implode_xstr) ||
skalberg@15531
   275
      Scan.one Symbol.is_blank >> K NONE;
wenzelm@18
   276
  in
wenzelm@4938
   277
    (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
wenzelm@24245
   278
      (toks, []) => map_filter I toks
wenzelm@4703
   279
    | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
wenzelm@18
   280
  end;
wenzelm@18
   281
wenzelm@18
   282
wenzelm@18
   283
wenzelm@18
   284
(** scan variables **)
wenzelm@18
   285
wenzelm@15991
   286
(* scan_indexname *)
wenzelm@15991
   287
wenzelm@15991
   288
local
wenzelm@18
   289
wenzelm@18
   290
fun scan_vname chrs =
wenzelm@18
   291
  let
wenzelm@15991
   292
    fun nat n [] = n
wenzelm@15991
   293
      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
wenzelm@18
   294
wenzelm@15991
   295
    fun idxname cs ds = (implode (rev cs), nat 0 ds);
wenzelm@15991
   296
    fun chop_idx [] ds = idxname [] 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@18
   303
    val scan =
wenzelm@15991
   304
      scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat 0) ~1;
wenzelm@18
   305
  in
wenzelm@18
   306
    (case scan chrs of
wenzelm@15991
   307
      ((cs, ~1), cs') => (chop_idx (rev cs) [], cs')
wenzelm@18
   308
    | ((cs, i), cs') => ((implode cs, i), cs'))
wenzelm@18
   309
  end;
wenzelm@18
   310
wenzelm@15991
   311
in
wenzelm@18
   312
berghofe@15443
   313
val scan_indexname =
berghofe@15443
   314
     $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i))
berghofe@15443
   315
  || scan_vname;
berghofe@15443
   316
wenzelm@15991
   317
end;
wenzelm@15991
   318
wenzelm@15991
   319
wenzelm@15991
   320
(* indexname *)
wenzelm@15991
   321
wenzelm@20313
   322
fun read_indexname s =
wenzelm@20313
   323
  (case Scan.read Symbol.stopper scan_indexname (Symbol.explode s) of
skalberg@15531
   324
    SOME xi => xi
wenzelm@20313
   325
  | _ => error ("Lexical error in variable name: " ^ quote s));
wenzelm@18
   326
wenzelm@18
   327
wenzelm@4703
   328
(* read_var *)
wenzelm@18
   329
wenzelm@550
   330
fun const c = Const (c, dummyT);
wenzelm@550
   331
fun free x = Free (x, dummyT);
wenzelm@550
   332
fun var xi = Var (xi, dummyT);
wenzelm@550
   333
wenzelm@4703
   334
fun read_var str =
wenzelm@18
   335
  let
wenzelm@18
   336
    val scan =
wenzelm@15991
   337
      $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var ||
wenzelm@23784
   338
      Scan.many Symbol.is_regular >> (free o implode);
wenzelm@15991
   339
  in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end;
wenzelm@15991
   340
wenzelm@15991
   341
wenzelm@15991
   342
(* read_variable *)
wenzelm@15991
   343
wenzelm@15991
   344
fun read_variable str =
wenzelm@15991
   345
  let val scan = $$ "?" |-- scan_indexname || scan_indexname
wenzelm@15991
   346
  in Scan.read Symbol.stopper scan (Symbol.explode str) end;
wenzelm@4587
   347
wenzelm@4587
   348
wenzelm@19002
   349
(* specific identifiers *)
wenzelm@5260
   350
wenzelm@19002
   351
val constN = "\\<^const>";
wenzelm@19002
   352
val fixedN = "\\<^fixed>";
wenzelm@19002
   353
wenzelm@5260
   354
wenzelm@20313
   355
(* read numbers *)
wenzelm@20313
   356
wenzelm@20313
   357
local
wenzelm@20313
   358
wenzelm@20313
   359
fun nat cs =
wenzelm@20313
   360
  Option.map (#1 o Library.read_int)
wenzelm@20313
   361
    (Scan.read Symbol.stopper scan_digits1 cs);
wenzelm@5860
   362
wenzelm@20313
   363
in
wenzelm@20313
   364
wenzelm@20313
   365
val read_nat = nat o Symbol.explode;
wenzelm@20313
   366
wenzelm@20313
   367
fun read_int s =
wenzelm@20313
   368
  (case Symbol.explode s of
wenzelm@20313
   369
    "-" :: cs => Option.map ~ (nat cs)
wenzelm@20313
   370
  | cs => nat cs);
wenzelm@20313
   371
wenzelm@20313
   372
end;
wenzelm@5860
   373
wenzelm@5860
   374
wenzelm@20096
   375
(* read_xnum: hex/bin/decimal *)
wenzelm@9326
   376
wenzelm@15991
   377
local
wenzelm@15991
   378
wenzelm@20096
   379
val ten = ord "0" + 10;
wenzelm@20096
   380
val a = ord "a";
wenzelm@20096
   381
val A = ord "A";
wenzelm@23802
   382
val _ = a > A orelse sys_error "Bad ASCII";
wenzelm@20096
   383
wenzelm@20096
   384
fun remap_hex c =
wenzelm@20096
   385
  let val x = ord c in
wenzelm@20096
   386
    if x >= a then chr (x - a + ten)
wenzelm@20096
   387
    else if x >= A then chr (x - A + ten)
wenzelm@20096
   388
    else c
wenzelm@20096
   389
  end;
wenzelm@15991
   390
wenzelm@21781
   391
fun leading_zeros ["0"] = 0
wenzelm@21781
   392
  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
wenzelm@21781
   393
  | leading_zeros _ = 0;
wenzelm@21781
   394
wenzelm@15991
   395
in
paulson@15965
   396
wenzelm@9326
   397
fun read_xnum str =
wenzelm@9326
   398
  let
wenzelm@20096
   399
    val (sign, radix, digs) =
wenzelm@20096
   400
      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
wenzelm@20096
   401
        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
wenzelm@20096
   402
      | "0" :: "b" :: cs => (1, 2, cs)
wenzelm@20096
   403
      | "-" :: cs => (~1, 10, cs)
wenzelm@20096
   404
      | cs => (1, 10, cs));
wenzelm@22574
   405
    val value = IntInf.fromInt sign * #1 (Library.read_intinf radix digs);
wenzelm@21781
   406
  in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
wenzelm@9326
   407
wenzelm@15991
   408
end;
wenzelm@15991
   409
wenzelm@9326
   410
wenzelm@7784
   411
(* read_ident(s) *)
wenzelm@7784
   412
wenzelm@7784
   413
fun read_idents str =
wenzelm@7784
   414
  let
wenzelm@21858
   415
    val blanks = Scan.many Symbol.is_blank;
wenzelm@23784
   416
    val junk = Scan.many Symbol.is_regular;
wenzelm@7784
   417
    val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk;
wenzelm@7784
   418
  in
wenzelm@7784
   419
    (case Scan.read Symbol.stopper idents (Symbol.explode str) of
skalberg@15531
   420
      SOME (ids, []) => ids
skalberg@15531
   421
    | SOME (_, bad) => error ("Bad identifier: " ^ quote (implode bad))
skalberg@15531
   422
    | NONE => error ("No identifier found in: " ^ quote str))
wenzelm@7784
   423
  end;
wenzelm@7784
   424
clasohm@0
   425
end;