src/Pure/General/name_space.ML
author wenzelm
Wed, 27 Apr 2011 17:44:06 +0200
changeset 42487 398d7d6bba42
parent 42466 bbce02fcba60
child 42493 01430341fc79
permissions -rw-r--r--
export Name_Space.entry_ord;
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
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    10
signature NAME_SPACE =
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    11
sig
9120
04a46ceace35 export hidden: string -> string;
wenzelm
parents: 8806
diff changeset
    12
  val hidden: string -> string
25225
e638164593bf export is_hidden;
wenzelm
parents: 25072
diff changeset
    13
  val is_hidden: string -> bool
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    14
  type T
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    15
  val empty: string -> T
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    16
  val kind_of: T -> string
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    17
  val the_entry: T -> string ->
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    18
    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
42487
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
    19
  val entry_ord: T -> string * string -> order
42379
26f64dddf2c6 tuned signature;
wenzelm
parents: 42375
diff changeset
    20
  val markup: T -> string -> Markup.T
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    21
  val is_concealed: T -> string -> bool
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    22
  val intern: T -> xstring -> string
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    23
  val long_names_default: bool Unsynchronized.ref
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    24
  val long_names_raw: Config.raw
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    25
  val long_names: bool Config.T
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    26
  val short_names_default: bool Unsynchronized.ref
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    27
  val short_names_raw: Config.raw
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    28
  val short_names: bool Config.T
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    29
  val unique_names_default: bool Unsynchronized.ref
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    30
  val unique_names_raw: Config.raw
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    31
  val unique_names: bool Config.T
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    32
  val extern: Proof.context -> T -> string -> xstring
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    33
  val hide: bool -> string -> T -> T
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    34
  val merge: T * T -> T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    35
  type naming
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
    36
  val default_naming: naming
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    37
  val conceal: naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    38
  val get_group: naming -> serial option
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    39
  val set_group: serial option -> naming -> naming
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    40
  val set_theory_name: string -> naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    41
  val new_group: naming -> naming
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    42
  val reset_group: naming -> naming
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    43
  val add_path: string -> naming -> naming
30418
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    44
  val root_path: naming -> naming
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    45
  val parent_path: naming -> naming
30469
de9e8f1d927c renamed sticky_prefix to mandatory_path;
wenzelm
parents: 30465
diff changeset
    46
  val mandatory_path: string -> naming -> naming
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
    47
  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
    48
  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
    49
  val full_name: naming -> binding -> string
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
    50
  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
    51
  val alias: naming -> binding -> string -> T -> T
24361
52a14669f9e9 tuned signature;
wenzelm
parents: 23668
diff changeset
    52
  type 'a table = T * 'a Symtab.table
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
    53
  val check: Proof.context -> 'a table -> xstring * Position.T -> string
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
    54
  val get: 'a table -> string -> 'a
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
    55
  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    56
  val empty_table: string -> 'a table
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    57
  val merge_tables: 'a table * 'a table -> 'a table
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
    58
  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
    59
    'a table * 'a table -> 'a table
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    60
  val dest_table: Proof.context -> 'a table -> (string * 'a) list
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    61
  val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    62
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    63
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
    64
structure Name_Space: NAME_SPACE =
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    65
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    66
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    67
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    68
(** name spaces **)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    69
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    70
(* hidden entries *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    71
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    72
fun hidden name = "??." ^ name;
29338
52a384648d13 separator, is_qualified
haftmann
parents: 29004
diff changeset
    73
val is_hidden = String.isPrefix "??.";
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    74
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    75
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    76
(* datatype entry *)
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    77
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    78
type entry =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
    79
 {concealed: bool,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    80
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    81
  theory_name: string,
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    82
  pos: Position.T,
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    83
  id: serial};
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    84
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    85
fun entry_markup def kind (name, {pos, id, ...}: entry) =
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    86
  let
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    87
    val props =
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    88
      if def then (Markup.defN, string_of_int id) :: Position.properties_of pos
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42135
diff changeset
    89
      else (Markup.refN, string_of_int id) :: Position.def_properties_of pos;
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    90
  in Markup.properties props (Markup.entity kind name) end;
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    91
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    92
fun print_entry def kind (name, entry) =
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    93
  quote (Markup.markup (entry_markup def kind (name, entry)) name);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    94
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    95
fun err_dup kind entry1 entry2 =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    96
  error ("Duplicate " ^ kind ^ " declaration " ^
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    97
    print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    98
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
    99
fun undefined kind name = "Undefined " ^ kind ^ ": " ^ quote name;
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   100
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   101
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   102
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   103
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   104
datatype T =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
   105
  Name_Space of
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   106
   {kind: string,
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   107
    internals: (string list * string list) Symtab.table,  (*visible, hidden*)
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   108
    entries: (xstring list * entry) Symtab.table};        (*externals, entry*)
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   109
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   110
fun make_name_space (kind, internals, entries) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   111
  Name_Space {kind = kind, internals = internals, entries = entries};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   112
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   113
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   114
  make_name_space (f (kind, internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   115
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   116
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   117
  (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   118
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   119
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   120
fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   121
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   122
fun kind_of (Name_Space {kind, ...}) = kind;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   123
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   124
fun the_entry (Name_Space {kind, entries, ...}) name =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   125
  (case Symtab.lookup entries name of
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   126
    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   127
  | SOME (_, entry) => entry);
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   128
42487
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
   129
fun entry_ord space = int_ord o pairself (#id o the_entry space);
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
   130
42379
26f64dddf2c6 tuned signature;
wenzelm
parents: 42375
diff changeset
   131
fun markup (Name_Space {kind, entries, ...}) name =
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   132
  (case Symtab.lookup entries name of
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   133
    NONE => Markup.malformed
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   134
  | SOME (_, entry) => entry_markup false kind (name, entry));
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   135
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   136
fun is_concealed space name = #concealed (the_entry space name);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   137
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   138
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   139
(* name accesses *)
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   140
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   141
fun lookup (Name_Space {internals, ...}) xname =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   142
  (case Symtab.lookup internals xname of
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   143
    NONE => (xname, true)
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   144
  | SOME ([], []) => (xname, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   145
  | SOME ([name], _) => (name, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   146
  | SOME (name :: _, _) => (name, false)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   147
  | SOME ([], name' :: _) => (hidden name', true));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   148
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   149
fun get_accesses (Name_Space {entries, ...}) name =
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   150
  (case Symtab.lookup entries name of
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   151
    NONE => [name]
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   152
  | SOME (externals, _) => externals);
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   153
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   154
fun valid_accesses (Name_Space {internals, ...}) name =
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   155
  Symtab.fold (fn (xname, (names, _)) =>
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   156
    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
   157
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   158
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   159
(* intern and extern *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   160
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   161
fun intern space xname = #1 (lookup space xname);
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   162
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   163
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   164
val long_names_default = Unsynchronized.ref false;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   165
val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   166
val long_names = Config.bool long_names_raw;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   167
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   168
val short_names_default = Unsynchronized.ref false;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   169
val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   170
val short_names = Config.bool short_names_raw;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   171
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   172
val unique_names_default = Unsynchronized.ref true;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   173
val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   174
val unique_names = Config.bool unique_names_raw;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   175
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   176
fun extern ctxt space name =
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   177
  let
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   178
    val long_names = Config.get ctxt long_names;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   179
    val short_names = Config.get ctxt short_names;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   180
    val unique_names = Config.get ctxt unique_names;
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   181
30277
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   182
    fun valid require_unique xname =
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   183
      let val (name', is_unique) = lookup space xname
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   184
      in name = name' andalso (not require_unique orelse is_unique) end;
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   185
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   186
    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
   187
      | 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
   188
  in
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   189
    if long_names then name
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   190
    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
   191
    else ext (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   192
  end;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   193
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   194
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   195
(* modify internals *)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   196
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   197
val del_name = map_internals o apfst o remove (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   198
fun del_name_extra name =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   199
  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   200
val add_name = map_internals o apfst o update (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   201
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
   202
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   203
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   204
(* hide *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   205
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   206
fun hide fully name space =
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   207
  if not (Long_Name.is_qualified name) then
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   208
    error ("Attempt to hide global name " ^ quote name)
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   209
  else if is_hidden name then
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   210
    error ("Attempt to hide hidden name " ^ quote name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   211
  else
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   212
    let val names = valid_accesses space name in
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   213
      space
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   214
      |> add_name' name name
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   215
      |> fold (del_name name)
33049
c38f02fdf35d curried inter as canonical list operation (beware of argument order)
haftmann
parents: 33038
diff changeset
   216
        (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
   217
      |> fold (del_name_extra name) (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   218
    end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   219
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
(* merge *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   222
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   223
fun merge
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   224
  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   225
    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
   226
  let
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   227
    val kind' =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   228
      if kind1 = kind2 then kind1
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   229
      else error ("Attempt to merge different kinds of name spaces " ^
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   230
        quote kind1 ^ " vs. " ^ quote kind2);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   231
    val internals' = (internals1, internals2) |> Symtab.join
30465
038839f111a1 renamed bind to define;
wenzelm
parents: 30438
diff changeset
   232
      (K (fn ((names1, names1'), (names2, names2')) =>
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   233
        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   234
        then raise Symtab.SAME
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   235
        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
   236
    val entries' = (entries1, entries2) |> Symtab.join
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   237
      (fn name => fn ((_, entry1), (_, entry2)) =>
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   238
        if #id entry1 = #id entry2 then raise Symtab.SAME
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   239
        else err_dup kind' (name, entry1) (name, entry2));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   240
  in make_name_space (kind', internals', entries') end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   241
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   242
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   243
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   244
(** naming contexts **)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   245
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   246
(* datatype naming *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   247
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   248
datatype naming = Naming of
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   249
 {conceal: bool,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   250
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   251
  theory_name: string,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   252
  path: (string * bool) list};
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   253
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   254
fun make_naming (conceal, group, theory_name, path) =
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   255
  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
   256
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   257
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
   258
  make_naming (f (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   259
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   260
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
   261
  (conceal, group, theory_name, f path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   262
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   263
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   264
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
   265
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   266
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
   267
  (true, group, theory_name, path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   268
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   269
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
   270
  (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   271
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   272
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   273
fun get_group (Naming {group, ...}) = group;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   274
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   275
fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   276
  (conceal, group, theory_name, path));
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   277
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   278
fun new_group naming = set_group (SOME (serial ())) naming;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   279
val reset_group = set_group NONE;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   280
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   281
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
   282
val root_path = map_path (fn _ => []);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   283
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
   284
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
   285
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   286
fun qualified_path mandatory binding = map_path (fn path =>
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   287
  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   288
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   289
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   290
(* full name *)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   291
41254
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 35679
diff changeset
   292
fun err_bad binding = error (Binding.bad binding);
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 35679
diff changeset
   293
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   294
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
   295
  | transform_binding _ = I;
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   296
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   297
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
   298
  let
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   299
    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
   300
    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
   301
    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
   302
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   303
    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
   304
    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
   305
    val spec = spec1 @ spec2;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   306
    val _ =
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   307
      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
   308
      andalso err_bad binding;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   309
  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
   310
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   311
fun full_name naming =
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   312
  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
   313
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   314
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   315
(* accesses *)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   316
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   317
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
   318
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   319
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
   320
and mandatory_prefixes1 [] = []
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   321
  | 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
   322
  | 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
   323
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   324
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
   325
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   326
fun accesses naming binding =
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   327
  let
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   328
    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
   329
    val sfxs = mandatory_suffixes spec;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   330
    val pfxs = mandatory_prefixes spec;
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   331
  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
   332
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   333
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   334
(* declaration *)
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   335
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   336
fun new_entry strict (name, (externals, entry)) =
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   337
  map_name_space (fn (kind, internals, entries) =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   338
    let
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   339
      val entries' =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   340
        (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   341
          handle Symtab.DUP dup =>
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   342
            err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   343
    in (kind, internals, entries') end);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   344
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   345
fun declare ctxt strict naming binding space =
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   346
  let
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   347
    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
   348
    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
   349
    val (accs, accs') = accesses naming binding;
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   350
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   351
    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
   352
    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
   353
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   354
    val pos = Position.default (Binding.pos_of binding);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   355
    val entry =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   356
     {concealed = concealed,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   357
      group = group,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   358
      theory_name = theory_name,
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   359
      pos = pos,
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   360
      id = serial ()};
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   361
    val space' = space
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   362
      |> fold (add_name name) accs
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   363
      |> new_entry strict (name, (accs', entry));
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   364
    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   365
  in (name, space') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   366
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   367
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   368
(* alias *)
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   369
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   370
fun alias naming binding name space =
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   371
  let
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   372
    val (accs, accs') = accesses naming binding;
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   373
    val space' = space
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   374
      |> fold (add_name name) accs
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   375
      |> map_name_space (fn (kind, internals, entries) =>
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   376
        let
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   377
          val _ = Symtab.defined entries name orelse error (undefined kind name);
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   378
          val entries' = entries
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   379
            |> Symtab.map_entry name (fn (externals, entry) =>
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   380
              (Library.merge (op =) (externals, accs'), entry))
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   381
        in (kind, internals, entries') end);
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   382
  in space' end;
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   383
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   384
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   385
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   386
(** name spaces coupled with symbol tables **)
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   387
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   388
type 'a table = T * 'a Symtab.table;
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   389
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   390
fun check ctxt (space, tab) (xname, pos) =
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   391
  let val name = intern space xname in
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   392
    if Symtab.defined tab name
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   393
    then (Context_Position.report ctxt pos (markup space name); name)
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   394
    else error (undefined (kind_of space) name ^ Position.str_of pos)
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   395
  end;
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   396
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   397
fun get (space, tab) name =
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   398
  (case Symtab.lookup tab name of
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   399
    SOME x => x
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   400
  | NONE => error (undefined (kind_of space) name));
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   401
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   402
fun define ctxt strict naming (binding, x) (space, tab) =
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   403
  let val (name, space') = declare ctxt strict naming binding space
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   404
  in (name, (space', Symtab.update (name, x) tab)) end;
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   405
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   406
fun empty_table kind = (empty kind, Symtab.empty);
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   407
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   408
fun merge_tables ((space1, tab1), (space2, tab2)) =
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   409
  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   410
28991
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   411
fun join_tables f ((space1, tab1), (space2, tab2)) =
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   412
  (merge (space1, space2), Symtab.join f (tab1, tab2));
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   413
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   414
fun ext_table ctxt (space, tab) =
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   415
  Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   416
  |> Library.sort_wrt (#2 o #1);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   417
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   418
fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   419
fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   420
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   421
end;
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   422