src/Pure/General/name_space.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 45412 7797f5351ec4
child 45666 d83797ef0d2d
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm@6118
     1
(*  Title:      Pure/General/name_space.ML
wenzelm@5012
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5012
     3
wenzelm@16137
     4
Generic name spaces with declared and hidden entries.  Unknown names
wenzelm@16341
     5
are considered global; no support for absolute addressing.
wenzelm@16137
     6
*)
wenzelm@16137
     7
wenzelm@26440
     8
type xstring = string;    (*external names*)
wenzelm@5012
     9
wenzelm@5012
    10
signature NAME_SPACE =
wenzelm@5012
    11
sig
wenzelm@9120
    12
  val hidden: string -> string
wenzelm@25225
    13
  val is_hidden: string -> bool
wenzelm@5012
    14
  type T
wenzelm@33096
    15
  val empty: string -> T
wenzelm@33096
    16
  val kind_of: T -> string
wenzelm@33164
    17
  val the_entry: T -> string ->
wenzelm@33164
    18
    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
wenzelm@42487
    19
  val entry_ord: T -> string * string -> order
wenzelm@42379
    20
  val markup: T -> string -> Markup.T
wenzelm@33157
    21
  val is_concealed: T -> string -> bool
wenzelm@16137
    22
  val intern: T -> xstring -> string
wenzelm@42669
    23
  val names_long_default: bool Unsynchronized.ref
wenzelm@42669
    24
  val names_long_raw: Config.raw
wenzelm@42669
    25
  val names_long: bool Config.T
wenzelm@42669
    26
  val names_short_default: bool Unsynchronized.ref
wenzelm@42669
    27
  val names_short_raw: Config.raw
wenzelm@42669
    28
  val names_short: bool Config.T
wenzelm@42669
    29
  val names_unique_default: bool Unsynchronized.ref
wenzelm@42669
    30
  val names_unique_raw: Config.raw
wenzelm@42669
    31
  val names_unique: bool Config.T
wenzelm@42358
    32
  val extern: Proof.context -> T -> string -> xstring
wenzelm@16137
    33
  val hide: bool -> string -> T -> T
wenzelm@5012
    34
  val merge: T * T -> T
wenzelm@16137
    35
  type naming
haftmann@28965
    36
  val default_naming: naming
wenzelm@33164
    37
  val conceal: naming -> naming
wenzelm@33724
    38
  val get_group: naming -> serial option
wenzelm@33724
    39
  val set_group: serial option -> naming -> naming
wenzelm@33164
    40
  val set_theory_name: string -> naming -> naming
wenzelm@33724
    41
  val new_group: naming -> naming
wenzelm@33724
    42
  val reset_group: naming -> naming
wenzelm@16137
    43
  val add_path: string -> naming -> naming
wenzelm@30418
    44
  val root_path: naming -> naming
wenzelm@30418
    45
  val parent_path: naming -> naming
wenzelm@30469
    46
  val mandatory_path: string -> naming -> naming
wenzelm@35200
    47
  val qualified_path: bool -> binding -> naming -> naming
wenzelm@33281
    48
  val transform_binding: naming -> binding -> binding
wenzelm@33157
    49
  val full_name: naming -> binding -> string
wenzelm@42375
    50
  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
wenzelm@35679
    51
  val alias: naming -> binding -> string -> T -> T
wenzelm@24361
    52
  type 'a table = T * 'a Symtab.table
wenzelm@43560
    53
  val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
wenzelm@42466
    54
  val get: 'a table -> string -> 'a
wenzelm@42375
    55
  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
wenzelm@33096
    56
  val empty_table: string -> 'a table
wenzelm@33091
    57
  val merge_tables: 'a table * 'a table -> 'a table
wenzelm@33097
    58
  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
wenzelm@33097
    59
    'a table * 'a table -> 'a table
wenzelm@42358
    60
  val dest_table: Proof.context -> 'a table -> (string * 'a) list
wenzelm@42358
    61
  val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
wenzelm@5012
    62
end;
wenzelm@5012
    63
wenzelm@33095
    64
structure Name_Space: NAME_SPACE =
wenzelm@5012
    65
struct
wenzelm@5012
    66
wenzelm@30412
    67
wenzelm@30412
    68
(** name spaces **)
wenzelm@30412
    69
wenzelm@30412
    70
(* hidden entries *)
wenzelm@5012
    71
wenzelm@16137
    72
fun hidden name = "??." ^ name;
haftmann@29338
    73
val is_hidden = String.isPrefix "??.";
wenzelm@16137
    74
wenzelm@5012
    75
wenzelm@33091
    76
(* datatype entry *)
wenzelm@33091
    77
wenzelm@33091
    78
type entry =
wenzelm@35679
    79
 {concealed: bool,
wenzelm@33164
    80
  group: serial option,
wenzelm@33164
    81
  theory_name: string,
wenzelm@33091
    82
  pos: Position.T,
wenzelm@33091
    83
  id: serial};
wenzelm@33091
    84
wenzelm@42135
    85
fun entry_markup def kind (name, {pos, id, ...}: entry) =
wenzelm@45412
    86
  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
wenzelm@42135
    87
wenzelm@42135
    88
fun print_entry def kind (name, entry) =
wenzelm@42135
    89
  quote (Markup.markup (entry_markup def kind (name, entry)) name);
wenzelm@33091
    90
wenzelm@33096
    91
fun err_dup kind entry1 entry2 =
wenzelm@33096
    92
  error ("Duplicate " ^ kind ^ " declaration " ^
wenzelm@42135
    93
    print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
wenzelm@33096
    94
wenzelm@42466
    95
fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
wenzelm@42466
    96
wenzelm@33091
    97
wenzelm@5012
    98
(* datatype T *)
wenzelm@5012
    99
wenzelm@5012
   100
datatype T =
wenzelm@33095
   101
  Name_Space of
wenzelm@33096
   102
   {kind: string,
wenzelm@33096
   103
    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
wenzelm@35679
   104
    entries: (xstring list * entry) Symtab.table};        (*externals, entry*)
wenzelm@33096
   105
wenzelm@33096
   106
fun make_name_space (kind, internals, entries) =
wenzelm@33096
   107
  Name_Space {kind = kind, internals = internals, entries = entries};
wenzelm@33096
   108
wenzelm@33096
   109
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
wenzelm@33096
   110
  make_name_space (f (kind, internals, entries));
wenzelm@33096
   111
wenzelm@33096
   112
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
wenzelm@33096
   113
  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
wenzelm@33096
   114
wenzelm@5012
   115
wenzelm@33096
   116
fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
wenzelm@33096
   117
wenzelm@33096
   118
fun kind_of (Name_Space {kind, ...}) = kind;
wenzelm@5012
   119
wenzelm@33096
   120
fun the_entry (Name_Space {kind, entries, ...}) name =
wenzelm@33096
   121
  (case Symtab.lookup entries name of
wenzelm@33096
   122
    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
wenzelm@35679
   123
  | SOME (_, entry) => entry);
wenzelm@33157
   124
wenzelm@42487
   125
fun entry_ord space = int_ord o pairself (#id o the_entry space);
wenzelm@42487
   126
wenzelm@42379
   127
fun markup (Name_Space {kind, entries, ...}) name =
wenzelm@42135
   128
  (case Symtab.lookup entries name of
wenzelm@42493
   129
    NONE => Markup.hilite
wenzelm@42135
   130
  | SOME (_, entry) => entry_markup false kind (name, entry));
wenzelm@42135
   131
wenzelm@33157
   132
fun is_concealed space name = #concealed (the_entry space name);
wenzelm@33096
   133
wenzelm@33096
   134
wenzelm@33096
   135
(* name accesses *)
wenzelm@33096
   136
wenzelm@33096
   137
fun lookup (Name_Space {internals, ...}) xname =
wenzelm@33096
   138
  (case Symtab.lookup internals xname of
wenzelm@16137
   139
    NONE => (xname, true)
wenzelm@30233
   140
  | SOME ([], []) => (xname, true)
wenzelm@30233
   141
  | SOME ([name], _) => (name, true)
wenzelm@30233
   142
  | SOME (name :: _, _) => (name, false)
wenzelm@30233
   143
  | SOME ([], name' :: _) => (hidden name', true));
wenzelm@8728
   144
wenzelm@33096
   145
fun get_accesses (Name_Space {entries, ...}) name =
wenzelm@33091
   146
  (case Symtab.lookup entries name of
wenzelm@25072
   147
    NONE => [name]
wenzelm@35679
   148
  | SOME (externals, _) => externals);
wenzelm@25072
   149
wenzelm@33096
   150
fun valid_accesses (Name_Space {internals, ...}) name =
wenzelm@33091
   151
  Symtab.fold (fn (xname, (names, _)) =>
wenzelm@33096
   152
    if not (null names) andalso hd names = name then cons xname else I) internals [];
wenzelm@8728
   153
wenzelm@8728
   154
wenzelm@16137
   155
(* intern and extern *)
wenzelm@16137
   156
wenzelm@16137
   157
fun intern space xname = #1 (lookup space xname);
wenzelm@16137
   158
wenzelm@42358
   159
wenzelm@42669
   160
val names_long_default = Unsynchronized.ref false;
wenzelm@42669
   161
val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
wenzelm@42669
   162
val names_long = Config.bool names_long_raw;
wenzelm@42358
   163
wenzelm@42669
   164
val names_short_default = Unsynchronized.ref false;
wenzelm@42669
   165
val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
wenzelm@42669
   166
val names_short = Config.bool names_short_raw;
wenzelm@42358
   167
wenzelm@42669
   168
val names_unique_default = Unsynchronized.ref true;
wenzelm@42669
   169
val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
wenzelm@42669
   170
val names_unique = Config.bool names_unique_raw;
wenzelm@42358
   171
wenzelm@42358
   172
fun extern ctxt space name =
wenzelm@16137
   173
  let
wenzelm@42669
   174
    val names_long = Config.get ctxt names_long;
wenzelm@42669
   175
    val names_short = Config.get ctxt names_short;
wenzelm@42669
   176
    val names_unique = Config.get ctxt names_unique;
wenzelm@42358
   177
wenzelm@30277
   178
    fun valid require_unique xname =
wenzelm@30277
   179
      let val (name', is_unique) = lookup space xname
wenzelm@30277
   180
      in name = name' andalso (not require_unique orelse is_unique) end;
wenzelm@8728
   181
wenzelm@26440
   182
    fun ext [] = if valid false name then name else hidden name
wenzelm@42669
   183
      | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
wenzelm@16137
   184
  in
wenzelm@42669
   185
    if names_long then name
wenzelm@42669
   186
    else if names_short then Long_Name.base_name name
wenzelm@30213
   187
    else ext (get_accesses space name)
wenzelm@16137
   188
  end;
wenzelm@16137
   189
wenzelm@5012
   190
wenzelm@33096
   191
(* modify internals *)
wenzelm@16137
   192
wenzelm@33096
   193
val del_name = map_internals o apfst o remove (op =);
wenzelm@33096
   194
fun del_name_extra name =
wenzelm@33096
   195
  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
wenzelm@33096
   196
val add_name = map_internals o apfst o update (op =);
wenzelm@33096
   197
val add_name' = map_internals o apsnd o update (op =);
wenzelm@25072
   198
wenzelm@8728
   199
wenzelm@8728
   200
(* hide *)
wenzelm@5012
   201
wenzelm@16137
   202
fun hide fully name space =
wenzelm@30359
   203
  if not (Long_Name.is_qualified name) then
wenzelm@8728
   204
    error ("Attempt to hide global name " ^ quote name)
wenzelm@8728
   205
  else if is_hidden name then
wenzelm@8728
   206
    error ("Attempt to hide hidden name " ^ quote name)
wenzelm@16137
   207
  else
wenzelm@16137
   208
    let val names = valid_accesses space name in
wenzelm@16137
   209
      space
wenzelm@16137
   210
      |> add_name' name name
wenzelm@30359
   211
      |> fold (del_name name)
haftmann@33049
   212
        (if fully then names else inter (op =) [Long_Name.base_name name] names)
wenzelm@30213
   213
      |> fold (del_name_extra name) (get_accesses space name)
wenzelm@16137
   214
    end;
wenzelm@5012
   215
wenzelm@5012
   216
wenzelm@16137
   217
(* merge *)
wenzelm@5012
   218
wenzelm@33096
   219
fun merge
wenzelm@33096
   220
  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
wenzelm@33096
   221
    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
wenzelm@25072
   222
  let
wenzelm@33096
   223
    val kind' =
wenzelm@33096
   224
      if kind1 = kind2 then kind1
wenzelm@33096
   225
      else error ("Attempt to merge different kinds of name spaces " ^
wenzelm@33096
   226
        quote kind1 ^ " vs. " ^ quote kind2);
wenzelm@33096
   227
    val internals' = (internals1, internals2) |> Symtab.join
wenzelm@30465
   228
      (K (fn ((names1, names1'), (names2, names2')) =>
wenzelm@33091
   229
        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
wenzelm@33091
   230
        then raise Symtab.SAME
wenzelm@30233
   231
        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
wenzelm@33091
   232
    val entries' = (entries1, entries2) |> Symtab.join
wenzelm@35679
   233
      (fn name => fn ((_, entry1), (_, entry2)) =>
wenzelm@33091
   234
        if #id entry1 = #id entry2 then raise Symtab.SAME
wenzelm@33096
   235
        else err_dup kind' (name, entry1) (name, entry2));
wenzelm@33096
   236
  in make_name_space (kind', internals', entries') end;
wenzelm@5012
   237
wenzelm@16137
   238
wenzelm@26440
   239
wenzelm@16137
   240
(** naming contexts **)
wenzelm@16137
   241
wenzelm@16137
   242
(* datatype naming *)
wenzelm@16137
   243
wenzelm@33164
   244
datatype naming = Naming of
wenzelm@33164
   245
 {conceal: bool,
wenzelm@33164
   246
  group: serial option,
wenzelm@33164
   247
  theory_name: string,
wenzelm@33164
   248
  path: (string * bool) list};
wenzelm@33164
   249
wenzelm@33164
   250
fun make_naming (conceal, group, theory_name, path) =
wenzelm@33164
   251
  Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
wenzelm@33164
   252
wenzelm@33164
   253
fun map_naming f (Naming {conceal, group, theory_name, path}) =
wenzelm@33164
   254
  make_naming (f (conceal, group, theory_name, path));
wenzelm@16137
   255
wenzelm@33164
   256
fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
wenzelm@33164
   257
  (conceal, group, theory_name, f path));
wenzelm@33164
   258
wenzelm@33164
   259
wenzelm@33164
   260
val default_naming = make_naming (false, NONE, "", []);
wenzelm@33157
   261
wenzelm@33164
   262
val conceal = map_naming (fn (_, group, theory_name, path) =>
wenzelm@33164
   263
  (true, group, theory_name, path));
wenzelm@33164
   264
wenzelm@33164
   265
fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
wenzelm@33164
   266
  (conceal, group, theory_name, path));
wenzelm@16137
   267
wenzelm@33724
   268
wenzelm@33724
   269
fun get_group (Naming {group, ...}) = group;
wenzelm@33724
   270
wenzelm@33724
   271
fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
wenzelm@33724
   272
  (conceal, group, theory_name, path));
wenzelm@33724
   273
wenzelm@33724
   274
fun new_group naming = set_group (SOME (serial ())) naming;
wenzelm@33724
   275
val reset_group = set_group NONE;
wenzelm@33724
   276
wenzelm@33157
   277
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
wenzelm@33157
   278
val root_path = map_path (fn _ => []);
wenzelm@33157
   279
val parent_path = map_path (perhaps (try (#1 o split_last)));
wenzelm@33157
   280
fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
wenzelm@33157
   281
wenzelm@35200
   282
fun qualified_path mandatory binding = map_path (fn path =>
wenzelm@35200
   283
  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
wenzelm@35200
   284
haftmann@28860
   285
wenzelm@30233
   286
(* full name *)
wenzelm@30233
   287
wenzelm@41254
   288
fun err_bad binding = error (Binding.bad binding);
wenzelm@41254
   289
wenzelm@33281
   290
fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
wenzelm@33281
   291
  | transform_binding _ = I;
wenzelm@33281
   292
wenzelm@33281
   293
fun name_spec (naming as Naming {path, ...}) raw_binding =
wenzelm@30233
   294
  let
wenzelm@33281
   295
    val binding = transform_binding naming raw_binding;
wenzelm@33281
   296
    val (concealed, prefix, name) = Binding.dest binding;
wenzelm@30438
   297
    val _ = Long_Name.is_qualified name andalso err_bad binding;
wenzelm@30412
   298
wenzelm@30412
   299
    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
wenzelm@30438
   300
    val spec2 = if name = "" then [] else [(name, true)];
wenzelm@30412
   301
    val spec = spec1 @ spec2;
wenzelm@30412
   302
    val _ =
wenzelm@30412
   303
      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
wenzelm@30412
   304
      andalso err_bad binding;
wenzelm@33157
   305
  in (concealed, if null spec2 then [] else spec) end;
wenzelm@30412
   306
wenzelm@33157
   307
fun full_name naming =
wenzelm@33164
   308
  name_spec naming #> #2 #> map #1 #> Long_Name.implode;
wenzelm@30412
   309
wenzelm@30412
   310
wenzelm@30412
   311
(* accesses *)
wenzelm@30412
   312
wenzelm@30412
   313
fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
wenzelm@30412
   314
wenzelm@30412
   315
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
wenzelm@30412
   316
and mandatory_prefixes1 [] = []
wenzelm@30412
   317
  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
wenzelm@30412
   318
  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
wenzelm@30412
   319
wenzelm@30412
   320
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
wenzelm@30412
   321
wenzelm@30522
   322
fun accesses naming binding =
wenzelm@30412
   323
  let
wenzelm@33157
   324
    val spec = #2 (name_spec naming binding);
wenzelm@30412
   325
    val sfxs = mandatory_suffixes spec;
wenzelm@30412
   326
    val pfxs = mandatory_prefixes spec;
wenzelm@30522
   327
  in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
wenzelm@30412
   328
wenzelm@30233
   329
wenzelm@30233
   330
(* declaration *)
haftmann@28860
   331
wenzelm@35679
   332
fun new_entry strict (name, (externals, entry)) =
wenzelm@33096
   333
  map_name_space (fn (kind, internals, entries) =>
wenzelm@33096
   334
    let
wenzelm@33096
   335
      val entries' =
wenzelm@35679
   336
        (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
wenzelm@33096
   337
          handle Symtab.DUP dup =>
wenzelm@35679
   338
            err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
wenzelm@33096
   339
    in (kind, internals, entries') end);
wenzelm@33091
   340
wenzelm@42375
   341
fun declare ctxt strict naming binding space =
wenzelm@30233
   342
  let
wenzelm@33164
   343
    val Naming {group, theory_name, ...} = naming;
wenzelm@33157
   344
    val (concealed, spec) = name_spec naming binding;
wenzelm@33157
   345
    val (accs, accs') = accesses naming binding;
wenzelm@33157
   346
wenzelm@33157
   347
    val name = Long_Name.implode (map fst spec);
wenzelm@30412
   348
    val _ = name = "" andalso err_bad binding;
wenzelm@33157
   349
wenzelm@42375
   350
    val pos = Position.default (Binding.pos_of binding);
wenzelm@33096
   351
    val entry =
wenzelm@35679
   352
     {concealed = concealed,
wenzelm@33164
   353
      group = group,
wenzelm@33164
   354
      theory_name = theory_name,
wenzelm@42375
   355
      pos = pos,
wenzelm@33096
   356
      id = serial ()};
wenzelm@35679
   357
    val space' = space
wenzelm@35679
   358
      |> fold (add_name name) accs
wenzelm@35679
   359
      |> new_entry strict (name, (accs', entry));
wenzelm@42375
   360
    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
wenzelm@30233
   361
  in (name, space') end;
haftmann@28860
   362
wenzelm@16137
   363
wenzelm@35679
   364
(* alias *)
wenzelm@35679
   365
wenzelm@35679
   366
fun alias naming binding name space =
wenzelm@35679
   367
  let
wenzelm@35679
   368
    val (accs, accs') = accesses naming binding;
wenzelm@35679
   369
    val space' = space
wenzelm@35679
   370
      |> fold (add_name name) accs
wenzelm@35679
   371
      |> map_name_space (fn (kind, internals, entries) =>
wenzelm@35679
   372
        let
wenzelm@42466
   373
          val _ = Symtab.defined entries name orelse error (undefined kind name);
wenzelm@35679
   374
          val entries' = entries
wenzelm@35679
   375
            |> Symtab.map_entry name (fn (externals, entry) =>
wenzelm@35679
   376
              (Library.merge (op =) (externals, accs'), entry))
wenzelm@35679
   377
        in (kind, internals, entries') end);
wenzelm@35679
   378
  in space' end;
wenzelm@35679
   379
wenzelm@35679
   380
wenzelm@16341
   381
wenzelm@43560
   382
(** name space coupled with symbol table **)
wenzelm@16341
   383
wenzelm@16341
   384
type 'a table = T * 'a Symtab.table;
wenzelm@16341
   385
wenzelm@42466
   386
fun check ctxt (space, tab) (xname, pos) =
wenzelm@42466
   387
  let val name = intern space xname in
wenzelm@43560
   388
    (case Symtab.lookup tab name of
wenzelm@43560
   389
      SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
wenzelm@43560
   390
    | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
wenzelm@42466
   391
  end;
wenzelm@42466
   392
wenzelm@42466
   393
fun get (space, tab) name =
wenzelm@42466
   394
  (case Symtab.lookup tab name of
wenzelm@42466
   395
    SOME x => x
wenzelm@42466
   396
  | NONE => error (undefined (kind_of space) name));
wenzelm@42466
   397
wenzelm@42375
   398
fun define ctxt strict naming (binding, x) (space, tab) =
wenzelm@42375
   399
  let val (name, space') = declare ctxt strict naming binding space
wenzelm@33091
   400
  in (name, (space', Symtab.update (name, x) tab)) end;
wenzelm@16341
   401
wenzelm@33096
   402
fun empty_table kind = (empty kind, Symtab.empty);
haftmann@28860
   403
wenzelm@33091
   404
fun merge_tables ((space1, tab1), (space2, tab2)) =
wenzelm@33091
   405
  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
wenzelm@16341
   406
haftmann@28991
   407
fun join_tables f ((space1, tab1), (space2, tab2)) =
haftmann@28991
   408
  (merge (space1, space2), Symtab.join f (tab1, tab2));
haftmann@28991
   409
wenzelm@42358
   410
fun ext_table ctxt (space, tab) =
wenzelm@42358
   411
  Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
wenzelm@16848
   412
  |> Library.sort_wrt (#2 o #1);
wenzelm@16848
   413
wenzelm@42358
   414
fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
wenzelm@42358
   415
fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
wenzelm@16341
   416
wenzelm@5012
   417
end;
wenzelm@30215
   418