src/Pure/General/name_space.ML
author wenzelm
Thu, 18 Feb 2010 20:46:46 +0100
changeset 35200 aaddb2b526d6
parent 33724 5ee13e0428d2
child 35432 b8863ee98f56
permissions -rw-r--r--
more systematic treatment of qualified names derived from binding;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5682
diff changeset
     1
(*  Title:      Pure/General/name_space.ML
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     3
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     4
Generic name spaces with declared and hidden entries.  Unknown names
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
     5
are considered global; no support for absolute addressing.
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     6
*)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
     7
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
     8
type xstring = string;    (*external names*)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
     9
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    10
signature BASIC_NAME_SPACE =
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    11
sig
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
    12
  val long_names: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
    13
  val short_names: bool Unsynchronized.ref
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
    14
  val unique_names: bool Unsynchronized.ref
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    15
end;
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    16
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    17
signature NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    18
sig
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    19
  include BASIC_NAME_SPACE
9120
04a46ceace35 export hidden: string -> string;
wenzelm
parents: 8806
diff changeset
    20
  val hidden: string -> string
25225
e638164593bf export is_hidden;
wenzelm
parents: 25072
diff changeset
    21
  val is_hidden: string -> bool
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    22
  type T
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    23
  val empty: string -> T
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    24
  val kind_of: T -> string
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    25
  val the_entry: T -> string ->
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    26
    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    27
  val is_concealed: T -> string -> bool
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    28
  val intern: T -> xstring -> string
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    29
  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
    30
    T -> string -> xstring
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    31
  val extern: T -> string -> xstring
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    32
  val hide: bool -> string -> T -> T
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    33
  val merge: T * T -> T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    34
  type naming
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
    35
  val default_naming: naming
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    36
  val conceal: naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    37
  val get_group: naming -> serial option
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    38
  val set_group: serial option -> naming -> naming
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    39
  val set_theory_name: string -> naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    40
  val new_group: naming -> naming
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    41
  val reset_group: naming -> naming
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    42
  val add_path: string -> naming -> naming
30418
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    43
  val root_path: naming -> naming
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    44
  val parent_path: naming -> naming
30469
de9e8f1d927c renamed sticky_prefix to mandatory_path;
wenzelm
parents: 30465
diff changeset
    45
  val mandatory_path: string -> naming -> naming
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
    46
  val qualified_path: bool -> binding -> naming -> naming
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
    47
  val transform_binding: naming -> binding -> binding
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    48
  val full_name: naming -> binding -> string
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    49
  val external_names: naming -> string -> string list
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    50
  val declare: bool -> naming -> binding -> T -> string * T
24361
52a14669f9e9 tuned signature;
wenzelm
parents: 23668
diff changeset
    51
  type 'a table = T * 'a Symtab.table
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    52
  val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    53
  val empty_table: string -> 'a table
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    54
  val merge_tables: 'a table * 'a table -> 'a table
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
    55
  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
    56
    'a table * 'a table -> 'a table
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
    57
  val dest_table: 'a table -> (string * 'a) list
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
    58
  val extern_table: 'a table -> (xstring * 'a) list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    59
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    60
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
    61
structure Name_Space: NAME_SPACE =
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    62
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    63
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    64
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    65
(** name spaces **)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    66
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    67
(* hidden entries *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    68
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    69
fun hidden name = "??." ^ name;
29338
52a384648d13 separator, is_qualified
haftmann
parents: 29004
diff changeset
    70
val is_hidden = String.isPrefix "??.";
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    71
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    72
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    73
(* datatype entry *)
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    74
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    75
type entry =
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    76
 {externals: xstring list,
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    77
  concealed: bool,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    78
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    79
  theory_name: string,
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    80
  pos: Position.T,
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    81
  id: serial};
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    82
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    83
fun str_of_entry def (name, {pos, id, ...}: entry) =
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    84
  let
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    85
    val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    86
    val props = occurrence :: Position.properties_of pos;
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    87
  in Markup.markup (Markup.properties props (Markup.entity name)) name end;
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    88
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    89
fun err_dup kind entry1 entry2 =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    90
  error ("Duplicate " ^ kind ^ " declaration " ^
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    91
    quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    92
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    93
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    94
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    95
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    96
datatype T =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
    97
  Name_Space of
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    98
   {kind: string,
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    99
    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   100
    entries: entry Symtab.table};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   101
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   102
fun make_name_space (kind, internals, entries) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   103
  Name_Space {kind = kind, internals = internals, entries = entries};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   104
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   105
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   106
  make_name_space (f (kind, internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   107
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   108
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   109
  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   110
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   111
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   112
fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   113
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   114
fun kind_of (Name_Space {kind, ...}) = kind;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   115
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   116
fun the_entry (Name_Space {kind, entries, ...}) name =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   117
  (case Symtab.lookup entries name of
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   118
    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   119
  | SOME {concealed, group, theory_name, pos, id, ...} =>
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   120
      {concealed = concealed, group = group, theory_name = theory_name, pos = pos, id = id});
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   121
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   122
fun is_concealed space name = #concealed (the_entry space name);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   123
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   124
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   125
(* name accesses *)
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   126
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   127
fun lookup (Name_Space {internals, ...}) xname =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   128
  (case Symtab.lookup internals xname of
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   129
    NONE => (xname, true)
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   130
  | SOME ([], []) => (xname, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   131
  | SOME ([name], _) => (name, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   132
  | SOME (name :: _, _) => (name, false)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   133
  | SOME ([], name' :: _) => (hidden name', true));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   134
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   135
fun get_accesses (Name_Space {entries, ...}) name =
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   136
  (case Symtab.lookup entries name of
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   137
    NONE => [name]
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   138
  | SOME {externals, ...} => externals);
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   139
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   140
fun valid_accesses (Name_Space {internals, ...}) name =
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   141
  Symtab.fold (fn (xname, (names, _)) =>
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   142
    if not (null names) andalso hd names = name then cons xname else I) internals [];
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   143
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   144
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   145
(* intern and extern *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   146
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   147
fun intern space xname = #1 (lookup space xname);
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   148
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   149
fun extern_flags {long_names, short_names, unique_names} space name =
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   150
  let
30277
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   151
    fun valid require_unique xname =
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   152
      let val (name', is_unique) = lookup space xname
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   153
      in name = name' andalso (not require_unique orelse is_unique) end;
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   154
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   155
    fun ext [] = if valid false name then name else hidden name
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   156
      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   157
  in
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   158
    if long_names then name
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   159
    else if short_names then Long_Name.base_name name
30213
3951aab916fd reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
wenzelm
parents: 29848
diff changeset
   160
    else ext (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   161
  end;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   162
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
   163
val long_names = Unsynchronized.ref false;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
   164
val short_names = Unsynchronized.ref false;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
   165
val unique_names = Unsynchronized.ref true;
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   166
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   167
fun extern space name =
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   168
  extern_flags
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   169
   {long_names = ! long_names,
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   170
    short_names = ! short_names,
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   171
    unique_names = ! unique_names} space name;
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   172
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   173
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   174
(* modify internals *)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   175
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   176
val del_name = map_internals o apfst o remove (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   177
fun del_name_extra name =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   178
  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   179
val add_name = map_internals o apfst o update (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   180
val add_name' = map_internals o apsnd o update (op =);
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   181
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   182
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   183
(* hide *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   184
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   185
fun hide fully name space =
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   186
  if not (Long_Name.is_qualified name) then
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   187
    error ("Attempt to hide global name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   188
  else if is_hidden name then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   189
    error ("Attempt to hide hidden name " ^ quote name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   190
  else
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   191
    let val names = valid_accesses space name in
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   192
      space
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   193
      |> add_name' name name
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   194
      |> fold (del_name name)
33049
c38f02fdf35d curried inter as canonical list operation (beware of argument order)
haftmann
parents: 33038
diff changeset
   195
        (if fully then names else inter (op =) [Long_Name.base_name name] names)
30213
3951aab916fd reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
wenzelm
parents: 29848
diff changeset
   196
      |> fold (del_name_extra name) (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   197
    end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   198
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   199
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   200
(* merge *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   201
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   202
fun merge
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   203
  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   204
    Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   205
  let
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   206
    val kind' =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   207
      if kind1 = kind2 then kind1
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   208
      else error ("Attempt to merge different kinds of name spaces " ^
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   209
        quote kind1 ^ " vs. " ^ quote kind2);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   210
    val internals' = (internals1, internals2) |> Symtab.join
30465
038839f111a1 renamed bind to define;
wenzelm
parents: 30438
diff changeset
   211
      (K (fn ((names1, names1'), (names2, names2')) =>
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   212
        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   213
        then raise Symtab.SAME
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   214
        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   215
    val entries' = (entries1, entries2) |> Symtab.join
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   216
      (fn name => fn (entry1, entry2) =>
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   217
        if #id entry1 = #id entry2 then raise Symtab.SAME
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   218
        else err_dup kind' (name, entry1) (name, entry2));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   219
  in make_name_space (kind', internals', entries') end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   220
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   221
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   222
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   223
(** naming contexts **)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   224
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   225
(* datatype naming *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   226
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   227
datatype naming = Naming of
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   228
 {conceal: bool,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   229
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   230
  theory_name: string,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   231
  path: (string * bool) list};
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   232
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   233
fun make_naming (conceal, group, theory_name, path) =
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   234
  Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   235
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   236
fun map_naming f (Naming {conceal, group, theory_name, path}) =
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   237
  make_naming (f (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   238
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   239
fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   240
  (conceal, group, theory_name, f path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   241
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   242
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   243
val default_naming = make_naming (false, NONE, "", []);
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   244
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   245
val conceal = map_naming (fn (_, group, theory_name, path) =>
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   246
  (true, group, theory_name, path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   247
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   248
fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   249
  (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   250
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   251
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   252
fun get_group (Naming {group, ...}) = group;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   253
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   254
fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   255
  (conceal, group, theory_name, path));
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   256
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   257
fun new_group naming = set_group (SOME (serial ())) naming;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   258
val reset_group = set_group NONE;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   259
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   260
fun add_path elems = map_path (fn path => path @ [(elems, false)]);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   261
val root_path = map_path (fn _ => []);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   262
val parent_path = map_path (perhaps (try (#1 o split_last)));
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   263
fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   264
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   265
fun qualified_path mandatory binding = map_path (fn path =>
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   266
  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   267
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   268
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   269
(* full name *)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   270
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   271
fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   272
  | transform_binding _ = I;
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   273
30465
038839f111a1 renamed bind to define;
wenzelm
parents: 30438
diff changeset
   274
fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   275
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   276
fun name_spec (naming as Naming {path, ...}) raw_binding =
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   277
  let
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   278
    val binding = transform_binding naming raw_binding;
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   279
    val (concealed, prefix, name) = Binding.dest binding;
30438
c2d49315b93b eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
wenzelm
parents: 30418
diff changeset
   280
    val _ = Long_Name.is_qualified name andalso err_bad binding;
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   281
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   282
    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
30438
c2d49315b93b eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
wenzelm
parents: 30418
diff changeset
   283
    val spec2 = if name = "" then [] else [(name, true)];
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   284
    val spec = spec1 @ spec2;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   285
    val _ =
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   286
      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   287
      andalso err_bad binding;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   288
  in (concealed, if null spec2 then [] else spec) end;
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   289
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   290
fun full_name naming =
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   291
  name_spec naming #> #2 #> map #1 #> Long_Name.implode;
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   292
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   293
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   294
(* accesses *)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   295
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   296
fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   297
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   298
fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   299
and mandatory_prefixes1 [] = []
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   300
  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   301
  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   302
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   303
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   304
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   305
fun accesses naming binding =
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   306
  let
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   307
    val spec = #2 (name_spec naming binding);
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   308
    val sfxs = mandatory_suffixes spec;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   309
    val pfxs = mandatory_prefixes spec;
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   310
  in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   311
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   312
fun external_names naming = #2 o accesses naming o Binding.qualified_name;
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   313
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   314
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   315
(* declaration *)
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   316
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   317
fun new_entry strict entry =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   318
  map_name_space (fn (kind, internals, entries) =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   319
    let
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   320
      val entries' =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   321
        (if strict then Symtab.update_new else Symtab.update) entry entries
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   322
          handle Symtab.DUP dup =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   323
            err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   324
    in (kind, internals, entries') end);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   325
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   326
fun declare strict naming binding space =
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   327
  let
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   328
    val Naming {group, theory_name, ...} = naming;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   329
    val (concealed, spec) = name_spec naming binding;
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   330
    val (accs, accs') = accesses naming binding;
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   331
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   332
    val name = Long_Name.implode (map fst spec);
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   333
    val _ = name = "" andalso err_bad binding;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   334
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   335
    val entry =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   336
     {externals = accs',
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   337
      concealed = concealed,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   338
      group = group,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   339
      theory_name = theory_name,
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
   340
      pos = Position.default (Binding.pos_of binding),
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   341
      id = serial ()};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   342
    val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   343
  in (name, space') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   344
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   345
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   346
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   347
(** name spaces coupled with symbol tables **)
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   348
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   349
type 'a table = T * 'a Symtab.table;
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   350
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   351
fun define strict naming (binding, x) (space, tab) =
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   352
  let val (name, space') = declare strict naming binding space
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   353
  in (name, (space', Symtab.update (name, x) tab)) end;
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   354
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   355
fun empty_table kind = (empty kind, Symtab.empty);
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   356
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   357
fun merge_tables ((space1, tab1), (space2, tab2)) =
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   358
  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   359
28991
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   360
fun join_tables f ((space1, tab1), (space2, tab2)) =
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   361
  (merge (space1, space2), Symtab.join f (tab1, tab2));
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   362
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   363
fun ext_table (space, tab) =
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   364
  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   365
  |> Library.sort_wrt (#2 o #1);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   366
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   367
fun dest_table tab = map (apfst #1) (ext_table tab);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   368
fun extern_table tab = map (apfst #2) (ext_table tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   369
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   370
end;
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   371
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
   372
structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30522
diff changeset
   373
open Basic_Name_Space;
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   374