src/Pure/General/name_space.ML
author wenzelm
Thu, 02 Apr 2015 20:07:05 +0200
changeset 59912 c7ba9b133bd4
parent 59889 30eef3e45bd0
child 59917 9830c944670f
permissions -rw-r--r--
export for informative purposes;
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
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55696
diff changeset
     4
Generic name spaces with declared and hidden entries; no support for
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55696
diff changeset
     5
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
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    12
  type T
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    13
  val empty: string -> T
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    14
  val kind_of: T -> string
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
    15
  val markup: T -> string -> Markup.T
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    16
  val the_entry: T -> string ->
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
    17
    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
42487
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
    18
  val entry_ord: T -> string * string -> order
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
    19
  val is_concealed: T -> string -> bool
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    20
  val intern: T -> xstring -> string
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    21
  val names_long_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    22
  val names_long: bool Config.T
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    23
  val names_short_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    24
  val names_short: bool Config.T
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    25
  val names_unique_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    26
  val names_unique: bool Config.T
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
    27
  val extern: Proof.context -> T -> string -> xstring
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
    28
  val extern_ord: Proof.context -> T -> string * string -> order
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
    29
  val extern_shortest: Proof.context -> T -> string -> xstring
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
    30
  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 51949
diff changeset
    31
  val pretty: Proof.context -> T -> string -> Pretty.T
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
    32
  val completion: Context.generic -> T -> xstring * Position.T -> Completion.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
59912
c7ba9b133bd4 export for informative purposes;
wenzelm
parents: 59889
diff changeset
    35
  val get_scopes: naming -> Binding.scope list
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
    36
  val get_scope: naming -> Binding.scope option
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
    37
  val new_scope: naming -> Binding.scope * naming
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
    38
  val private: Binding.scope -> naming -> naming
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
    39
  val concealed: naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    40
  val get_group: naming -> serial option
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    41
  val set_group: serial option -> naming -> naming
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    42
  val set_theory_name: string -> naming -> naming
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    43
  val new_group: naming -> naming
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
    44
  val reset_group: naming -> naming
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    45
  val add_path: string -> naming -> naming
30418
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    46
  val root_path: naming -> naming
b5044aca0729 add_path: discontinued special meaning of "//", "/", "..";
wenzelm
parents: 30412
diff changeset
    47
  val parent_path: naming -> naming
30469
de9e8f1d927c renamed sticky_prefix to mandatory_path;
wenzelm
parents: 30465
diff changeset
    48
  val mandatory_path: string -> naming -> naming
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
    49
  val qualified_path: bool -> binding -> naming -> naming
58668
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
    50
  val global_naming: naming
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    51
  val local_naming: naming
59887
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
    52
  val transform_naming: naming -> naming -> naming
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
    53
  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
    54
  val full_name: naming -> binding -> string
47021
f35f654f297d clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents: 47005
diff changeset
    55
  val base_name: binding -> string
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
    56
  val hide: bool -> string -> T -> T
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
    57
  val alias: naming -> binding -> string -> T -> T
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    58
  val naming_of: Context.generic -> naming
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    59
  val map_naming: (naming -> naming) -> Context.generic -> Context.generic
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    60
  val declare: Context.generic -> bool -> binding -> T -> string * T
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    61
  type 'a table
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
    62
  val change_base: bool -> 'a table -> 'a table
56139
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
    63
  val change_ignore: 'a table -> 'a table
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    64
  val space_of_table: 'a table -> T
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
    65
  val check_reports: Context.generic -> 'a table ->
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
    66
    xstring * Position.T list -> (string * Position.report list) * 'a
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    67
  val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
59883
12a89103cae6 tuned signature;
wenzelm
parents: 59881
diff changeset
    68
  val defined: 'a table -> string -> bool
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
    69
  val lookup: 'a table -> string -> 'a option
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    70
  val lookup_key: 'a table -> string -> (string * 'a) option
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
    71
  val get: 'a table -> string -> 'a
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    72
  val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    73
  val alias_table: naming -> binding -> string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    74
  val hide_table: bool -> string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    75
  val del_table: string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    76
  val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    77
  val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    78
  val empty_table: string -> 'a table
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    79
  val merge_tables: 'a table * 'a table -> 'a table
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
    80
  val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 33096
diff changeset
    81
    'a table * 'a table -> 'a table
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    82
  val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    83
  val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    84
  val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    85
  val markup_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    86
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    87
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
    88
structure Name_Space: NAME_SPACE =
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    89
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    90
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    91
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    92
(** name spaces **)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    93
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    94
(* datatype entry *)
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    95
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    96
type entry =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
    97
 {concealed: bool,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    98
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    99
  theory_name: string,
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   100
  pos: Position.T,
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
   101
  serial: serial};
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   102
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
   103
fun entry_markup def kind (name, {pos, serial, ...}: entry) =
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
   104
  Markup.properties (Position.entity_properties_of def serial pos) (Markup.entity kind name);
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   105
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   106
fun print_entry_ref kind (name, entry) =
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   107
  quote (Markup.markup (entry_markup false kind (name, entry)) name);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   108
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   109
fun err_dup kind entry1 entry2 pos =
56038
0e2dec666152 tuned messages -- in accordance to Isabelle/Scala;
wenzelm
parents: 56025
diff changeset
   110
  error ("Duplicate " ^ plain_words kind ^ " declaration " ^
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   111
    print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   112
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   113
56164
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   114
(* internal names *)
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   115
59881
wenzelm
parents: 59874
diff changeset
   116
type internals = (string list * string list) Change_Table.T;
56164
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   117
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   118
fun map_internals f xname : internals -> internals =
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   119
  Change_Table.map_default (xname, ([], [])) f;
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   120
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   121
val del_name = map_internals o apfst o remove (op =);
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   122
fun del_name_extra name =
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   123
  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   124
val add_name = map_internals o apfst o update (op =);
59881
wenzelm
parents: 59874
diff changeset
   125
fun hide_name name = map_internals (apsnd (update (op =) name)) name;
56164
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   126
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   127
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   128
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   129
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   130
datatype T =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
   131
  Name_Space of
59881
wenzelm
parents: 59874
diff changeset
   132
   {kind: string,
wenzelm
parents: 59874
diff changeset
   133
    internals: internals,  (*xname -> visible, hidden*)
56164
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   134
    entries: (xstring list * entry) Change_Table.T};  (*name -> externals, entry*)
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   135
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   136
fun make_name_space (kind, internals, entries) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   137
  Name_Space {kind = kind, internals = internals, entries = entries};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   138
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   139
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   140
  make_name_space (f (kind, internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   141
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   142
fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   143
  (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   144
56139
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   145
val change_ignore_space = map_name_space (fn (kind, internals, entries) =>
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   146
  (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries));
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   147
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   148
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   149
fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   150
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   151
fun kind_of (Name_Space {kind, ...}) = kind;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   152
42379
26f64dddf2c6 tuned signature;
wenzelm
parents: 42375
diff changeset
   153
fun markup (Name_Space {kind, entries, ...}) name =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   154
  (case Change_Table.lookup entries name of
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49816
diff changeset
   155
    NONE => Markup.intensify
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   156
  | SOME (_, entry) => entry_markup false kind (name, entry));
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   157
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   158
fun undefined (space as Name_Space {kind, entries, ...}) bad =
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   159
  let
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   160
    val (prfx, sfx) =
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   161
      (case Long_Name.dest_hidden bad of
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   162
        SOME name =>
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   163
          if Change_Table.defined entries name
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   164
          then ("Inaccessible", Markup.markup (markup space name) (quote name))
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   165
          else ("Undefined", quote name)
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   166
      | NONE => ("Undefined", quote bad));
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   167
  in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   168
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   169
fun the_entry (space as Name_Space {entries, ...}) name =
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   170
  (case Change_Table.lookup entries name of
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   171
    NONE => error (undefined space name)
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   172
  | SOME (_, entry) => entry);
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   173
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   174
fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   175
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   176
fun is_concealed space name = #concealed (the_entry space name);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   177
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   178
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   179
(* intern *)
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   180
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   181
fun intern' (Name_Space {internals, ...}) xname =
59885
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   182
  (case the_default ([], []) (Change_Table.lookup internals xname) of
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   183
    ([name], _) => (name, true)
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   184
  | (name :: _, _) => (name, false)
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   185
  | ([], []) => (Long_Name.hidden xname, true)
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   186
  | ([], name' :: _) => (Long_Name.hidden name', true));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   187
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   188
val intern = #1 oo intern';
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   189
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   190
fun get_accesses (Name_Space {entries, ...}) name =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   191
  (case Change_Table.lookup entries name of
59885
3470a265d404 subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;
wenzelm
parents: 59884
diff changeset
   192
    NONE => []
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   193
  | SOME (externals, _) => externals);
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   194
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   195
fun valid_accesses (Name_Space {internals, ...}) name =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   196
  Change_Table.fold (fn (xname, (names, _)) =>
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   197
    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
   198
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   199
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   200
(* extern *)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   201
56438
7f6b2634d853 more source positions;
wenzelm
parents: 56168
diff changeset
   202
val names_long_raw = Config.declare_option ("names_long", @{here});
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   203
val names_long = Config.bool names_long_raw;
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   204
56438
7f6b2634d853 more source positions;
wenzelm
parents: 56168
diff changeset
   205
val names_short_raw = Config.declare_option ("names_short", @{here});
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   206
val names_short = Config.bool names_short_raw;
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   207
56438
7f6b2634d853 more source positions;
wenzelm
parents: 56168
diff changeset
   208
val names_unique_raw = Config.declare_option ("names_unique", @{here});
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   209
val names_unique = Config.bool names_unique_raw;
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   210
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   211
fun extern ctxt space name =
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   212
  let
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   213
    val names_long = Config.get ctxt names_long;
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   214
    val names_short = Config.get ctxt names_short;
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   215
    val names_unique = Config.get ctxt names_unique;
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   216
30277
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   217
    fun valid require_unique xname =
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   218
      let val (name', is_unique) = intern' space xname
30277
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   219
      in name = name' andalso (not require_unique orelse is_unique) end;
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   220
55669
4612c450b59c tuned signature;
wenzelm
parents: 53539
diff changeset
   221
    fun ext [] = if valid false name then name else Long_Name.hidden name
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   222
      | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   223
  in
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   224
    if names_long then name
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   225
    else if names_short 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
   226
    else ext (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   227
  end;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   228
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58668
diff changeset
   229
fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   230
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   231
fun extern_shortest ctxt =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   232
  extern
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   233
    (ctxt
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   234
      |> Config.put names_long false
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   235
      |> Config.put names_short false
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   236
      |> Config.put names_unique false);
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   237
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   238
fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   239
fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   240
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   241
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   242
(* completion *)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   243
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   244
fun completion context space (xname, pos) =
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   245
  Completion.make (xname, pos) (fn completed =>
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   246
    let
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56160
diff changeset
   247
      fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
59888
27e4d0ab0948 tuned signature;
wenzelm
parents: 59887
diff changeset
   248
        (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56160
diff changeset
   249
          EQUAL =>
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58668
diff changeset
   250
            (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56160
diff changeset
   251
              EQUAL => string_ord (xname1, xname2)
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56160
diff changeset
   252
            | ord => ord)
56024
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   253
        | ord => ord);
55975
9962ca0875c9 no completion of concealed names;
wenzelm
parents: 55962
diff changeset
   254
      val Name_Space {kind, internals, ...} = space;
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   255
      val ext = extern_shortest (Context.proof_of context) space;
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   256
    in
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   257
      Change_Table.fold
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   258
        (fn (a, (name :: _, _)) =>
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   259
            if completed a andalso not (is_concealed space name) then
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   260
              let val a' = ext name
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   261
              in if a = a' then cons (a', (kind, name)) else I end
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   262
            else I
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   263
          | _ => I) internals []
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   264
      |> sort_distinct result_ord
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59058
diff changeset
   265
    end);
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 51949
diff changeset
   266
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   267
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   268
(* merge *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   269
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   270
fun merge
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   271
  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   272
    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
   273
  let
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   274
    val kind' =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   275
      if kind1 = kind2 then kind1
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   276
      else error ("Attempt to merge different kinds of name spaces " ^
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   277
        quote kind1 ^ " vs. " ^ quote kind2);
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   278
    val internals' = (internals1, internals2) |> Change_Table.join
30465
038839f111a1 renamed bind to define;
wenzelm
parents: 30438
diff changeset
   279
      (K (fn ((names1, names1'), (names2, names2')) =>
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   280
        if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   281
        then raise Change_Table.SAME
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   282
        else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   283
    val entries' = (entries1, entries2) |> Change_Table.join
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   284
      (fn name => fn ((_, entry1), (_, entry2)) =>
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
   285
        if #serial entry1 = #serial entry2 then raise Change_Table.SAME
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   286
        else err_dup kind' (name, entry1) (name, entry2) Position.none);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   287
  in make_name_space (kind', internals', entries') end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   288
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   289
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   290
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   291
(** naming context **)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   292
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   293
(* datatype naming *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   294
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   295
datatype naming = Naming of
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   296
 {scopes: Binding.scope list,
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   297
  private: Binding.scope option,
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
   298
  concealed: bool,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   299
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   300
  theory_name: string,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   301
  path: (string * bool) list};
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   302
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   303
fun make_naming (scopes, private, concealed, group, theory_name, path) =
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   304
  Naming {scopes = scopes, private = private, concealed = concealed,
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   305
    group = group, theory_name = theory_name, path = path};
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   306
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   307
fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   308
  make_naming (f (scopes, private, concealed, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   309
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   310
fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   311
  (scopes, private, concealed, group, theory_name, f path));
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   312
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   313
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   314
fun get_scopes (Naming {scopes, ...}) = scopes;
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   315
val get_scope = try hd o get_scopes;
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   316
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   317
fun new_scope naming =
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   318
  let
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   319
    val scope = Binding.new_scope ();
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   320
    val naming' =
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   321
      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   322
        (scope :: scopes, private, concealed, group, theory_name, path));
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   323
  in (scope, naming') end;
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   324
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   325
fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   326
  (scopes, SOME scope, concealed, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   327
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   328
val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   329
  (scopes, private, true, group, theory_name, path));
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   330
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   331
fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   332
  (scopes, private, concealed, group, theory_name, path));
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   333
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   334
fun get_group (Naming {group, ...}) = group;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   335
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   336
fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   337
  (scopes, private, concealed, group, theory_name, path));
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   338
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   339
fun new_group naming = set_group (SOME (serial ())) naming;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   340
val reset_group = set_group NONE;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   341
59874
3ecb48ce92d7 tuned signature;
wenzelm
parents: 59859
diff changeset
   342
fun get_path (Naming {path, ...}) = path;
3ecb48ce92d7 tuned signature;
wenzelm
parents: 59859
diff changeset
   343
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   344
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
   345
val root_path = map_path (fn _ => []);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   346
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
   347
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
   348
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   349
fun qualified_path mandatory binding = map_path (fn path =>
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   350
  path @ Binding.path_of (Binding.qualified mandatory "" binding));
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   351
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   352
val global_naming = make_naming ([], NONE, false, NONE, "", []);
58668
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
   353
val local_naming = global_naming |> add_path Long_Name.localN;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   354
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   355
59887
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   356
(* visibility flags *)
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   357
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   358
fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   359
  fold private (the_list private') #>
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   360
  concealed' ? concealed;
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   361
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
   362
fun transform_binding (Naming {private, concealed, ...}) =
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   363
  Binding.private_default private #>
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
   364
  concealed ? Binding.concealed;
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   365
59887
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   366
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   367
(* full name *)
43dc3c660f41 more visibility flags on background naming;
wenzelm
parents: 59886
diff changeset
   368
59874
3ecb48ce92d7 tuned signature;
wenzelm
parents: 59859
diff changeset
   369
fun name_spec naming binding =
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   370
  Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   371
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   372
fun full_name naming =
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   373
  name_spec naming #> #spec #> 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
   374
58668
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
   375
val base_name = full_name global_naming #> Long_Name.base_name;
47021
f35f654f297d clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents: 47005
diff changeset
   376
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   377
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   378
(* accesses *)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   379
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   380
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
   381
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   382
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
   383
and mandatory_prefixes1 [] = []
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   384
  | 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
   385
  | 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
   386
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   387
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
   388
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   389
fun accesses naming binding =
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   390
  (case name_spec naming binding of
59886
e0dc738eb08c support for explicit scope of private entries;
wenzelm
parents: 59885
diff changeset
   391
    {accessible = false, ...} => ([], [])
59858
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   392
  | {spec, ...} =>
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   393
      let
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   394
        val sfxs = mandatory_suffixes spec;
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   395
        val pfxs = mandatory_prefixes spec;
890b68e1e8b6 support for strictly private name space entries;
wenzelm
parents: 59812
diff changeset
   396
      in apply2 (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
   397
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   398
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   399
(* hide *)
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   400
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   401
fun hide fully name space =
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   402
  space |> map_name_space (fn (kind, internals, entries) =>
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   403
    let
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   404
      val _ = the_entry space name;
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   405
      val names = valid_accesses space name;
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   406
      val internals' = internals
59881
wenzelm
parents: 59874
diff changeset
   407
        |> hide_name name
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   408
        |> fold (del_name name)
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   409
          (if fully then names else inter (op =) [Long_Name.base_name name] names)
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   410
        |> fold (del_name_extra name) (get_accesses space name);
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   411
    in (kind, internals', entries) end);
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   412
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   413
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   414
(* alias *)
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   415
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   416
fun alias naming binding name space =
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   417
  space |> map_name_space (fn (kind, internals, entries) =>
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   418
    let
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   419
      val _ = the_entry space name;
56168
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   420
      val (accs, accs') = accesses naming binding;
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   421
      val internals' = internals |> fold (add_name name) accs;
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   422
      val entries' = entries
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   423
        |> Change_Table.map_entry name (fn (externals, entry) =>
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   424
          (Library.merge (op =) (externals, accs'), entry))
088b64497a61 more uniform alias vs. hide: proper check, allow to hide global names as well;
wenzelm
parents: 56164
diff changeset
   425
    in (kind, internals', entries') end);
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   426
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   427
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   428
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   429
(** context naming **)
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   430
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   431
structure Data_Args =
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   432
struct
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   433
  type T = naming;
58668
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
   434
  val empty = global_naming;
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
   435
  fun extend _ = global_naming;
1891f17c6124 tuned signature;
wenzelm
parents: 57899
diff changeset
   436
  fun merge _ = global_naming;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   437
  fun init _ = local_naming;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   438
end;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   439
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   440
structure Global_Naming = Theory_Data(Data_Args);
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   441
structure Local_Naming = Proof_Data(Data_Args);
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   442
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   443
fun naming_of (Context.Theory thy) = Global_Naming.get thy
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   444
  | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   445
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   446
fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   447
  | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   448
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   449
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   450
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   451
(** entry definition **)
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   452
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   453
(* declaration *)
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   454
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   455
fun declare context strict binding space =
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   456
  let
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   457
    val naming = naming_of context;
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   458
    val Naming {group, theory_name, ...} = naming;
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
   459
    val {concealed, spec, ...} = name_spec naming binding;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   460
    val (accs, accs') = accesses naming binding;
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   461
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   462
    val name = Long_Name.implode (map fst spec);
59874
3ecb48ce92d7 tuned signature;
wenzelm
parents: 59859
diff changeset
   463
    val _ = name = "" andalso error (Binding.bad binding);
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   464
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 49358
diff changeset
   465
    val (proper_pos, pos) = Position.default (Binding.pos_of binding);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   466
    val entry =
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59858
diff changeset
   467
     {concealed = concealed,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   468
      group = group,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   469
      theory_name = theory_name,
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   470
      pos = pos,
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56438
diff changeset
   471
      serial = serial ()};
56164
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   472
    val space' =
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   473
      space |> map_name_space (fn (kind, internals, entries) =>
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   474
        let
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   475
          val internals' = internals |> fold (add_name name) accs;
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   476
          val entries' =
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   477
            (if strict then Change_Table.update_new else Change_Table.update)
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   478
              (name, (accs', entry)) entries
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   479
            handle Change_Table.DUP dup =>
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   480
              err_dup kind (dup, #2 (the (Change_Table.lookup entries dup)))
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   481
                (name, entry) (#pos entry);
c7805a88f952 minor tuning;
wenzelm
parents: 56162
diff changeset
   482
        in (kind, internals', entries') end);
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   483
    val _ =
56160
d348378ddf47 tuned -- avoid vacuous reports;
wenzelm
parents: 56139
diff changeset
   484
      if proper_pos andalso Context_Position.is_reported_generic context pos then
d348378ddf47 tuned -- avoid vacuous reports;
wenzelm
parents: 56139
diff changeset
   485
        Position.report pos (entry_markup true (kind_of space) (name, entry))
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 49358
diff changeset
   486
      else ();
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   487
  in (name, space') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   488
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   489
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   490
(* definition in symbol table *)
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   491
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   492
datatype 'a table = Table of T * 'a Change_Table.T;
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   493
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   494
fun change_base begin (Table (space, tab)) =
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   495
  Table (change_base_space begin space, Change_Table.change_base begin tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   496
56139
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   497
fun change_ignore (Table (space, tab)) =
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   498
  Table (change_ignore_space space, Change_Table.change_ignore tab);
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   499
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   500
fun space_of_table (Table (space, _)) = space;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   501
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   502
fun check_reports context (Table (space, tab)) (xname, ps) =
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   503
  let val name = intern space xname in
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   504
    (case Change_Table.lookup tab name of
55696
de2668c50403 tuned whitespace;
wenzelm
parents: 55694
diff changeset
   505
      SOME x =>
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   506
        let
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   507
          val reports =
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   508
            filter (Context_Position.is_reported_generic context) ps
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   509
            |> map (fn pos => (pos, markup space name));
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   510
        in ((name, reports), x) end
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   511
    | NONE =>
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   512
        let
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   513
          val completions = map (fn pos => completion context space (xname, pos)) ps;
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   514
        in
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   515
          error (undefined space name ^ Position.here_list ps ^
55957
cffb46aea3d1 more compact Markup.markup_report: message body may consist of multiple elements;
wenzelm
parents: 55956
diff changeset
   516
            Markup.markup_report (implode (map Completion.reported_text completions)))
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   517
        end)
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   518
  end;
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   519
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   520
fun check context table (xname, pos) =
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   521
  let
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   522
    val ((name, reports), x) = check_reports context table (xname, [pos]);
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   523
    val _ = Position.reports reports;
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   524
  in (name, x) end;
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   525
59883
12a89103cae6 tuned signature;
wenzelm
parents: 59881
diff changeset
   526
fun defined (Table (_, tab)) name = Change_Table.defined tab name;
59884
bbf49d7dfd6f tuned signature;
wenzelm
parents: 59883
diff changeset
   527
fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   528
fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   529
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   530
fun get table name =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   531
  (case lookup_key table name of
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   532
    SOME (_, x) => x
59889
30eef3e45bd0 tuned message;
wenzelm
parents: 59888
diff changeset
   533
  | NONE => error (undefined (space_of_table table) name));
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   534
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   535
fun define context strict (binding, x) (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   536
  let
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   537
    val (name, space') = declare context strict binding space;
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   538
    val tab' = Change_Table.update (name, x) tab;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   539
  in (name, Table (space', tab')) end;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   540
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   541
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   542
(* derived table operations *)
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   543
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   544
fun alias_table naming binding name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   545
  Table (alias naming binding name space, tab);
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   546
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   547
fun hide_table fully name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   548
  Table (hide fully name space, tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   549
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   550
fun del_table name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   551
  let
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   552
    val space' = hide true name space handle ERROR _ => space;
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   553
    val tab' = Change_Table.delete_safe name tab;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   554
  in Table (space', tab') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   555
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   556
fun map_table_entry name f (Table (space, tab)) =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   557
  Table (space, Change_Table.map_entry name f tab);
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   558
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   559
fun fold_table f (Table (_, tab)) = Change_Table.fold f tab;
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   560
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   561
fun empty_table kind = Table (empty kind, Change_Table.empty);
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   562
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   563
fun merge_tables (Table (space1, tab1), Table (space2, tab2)) =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   564
  Table (merge (space1, space2), Change_Table.merge (K true) (tab1, tab2));
28991
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   565
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   566
fun join_tables f (Table (space1, tab1), Table (space2, tab2)) =
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   567
  Table (merge (space1, space2), Change_Table.join f (tab1, tab2));
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   568
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   569
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   570
(* present table content *)
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   571
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   572
fun extern_entries ctxt space entries =
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   573
  fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   574
  |> Library.sort_wrt (#2 o #1);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   575
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   576
fun markup_entries ctxt space entries =
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   577
  extern_entries ctxt space entries
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   578
  |> map (fn ((name, xname), x) => ((markup space name, xname), x));
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   579
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   580
fun extern_table ctxt (Table (space, tab)) = extern_entries ctxt space (Change_Table.dest tab);
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 56052
diff changeset
   581
fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   582
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   583
end;