src/Pure/General/name_space.ML
author wenzelm
Sat, 15 Mar 2014 11:57:55 +0100
changeset 56160 d348378ddf47
parent 56139 b7add947a6ef
child 56162 ea6303e2261b
permissions -rw-r--r--
tuned -- avoid vacuous reports;
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
46869
26a9a4e0a631 more direct Name_Space.defined_entry;
wenzelm
parents: 45666
diff changeset
    15
  val defined_entry: T -> string -> bool
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    16
  val the_entry: T -> string ->
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    17
    {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
    18
  val entry_ord: T -> string * string -> order
42379
26f64dddf2c6 tuned signature;
wenzelm
parents: 42375
diff changeset
    19
  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
    20
  val is_concealed: T -> string -> bool
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    21
  val intern: T -> xstring -> string
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    22
  val names_long_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    23
  val names_long: bool Config.T
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    24
  val names_short_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    25
  val names_short: bool Config.T
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    26
  val names_unique_raw: Config.raw
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
    27
  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
    28
  val extern: Proof.context -> T -> string -> xstring
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
    29
  val extern_ord: Proof.context -> T -> string * string -> order
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
    30
  val extern_shortest: Proof.context -> T -> string -> xstring
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
    31
  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 51949
diff changeset
    32
  val pretty: Proof.context -> T -> string -> Pretty.T
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
    33
  val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    34
  val hide: bool -> string -> T -> T
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    35
  val merge: T * T -> T
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
    36
  type 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
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    48
  val default_naming: naming
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
    49
  val local_naming: naming
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
    50
  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
    51
  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
    52
  val base_name: binding -> string
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
    53
  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
    54
  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
    55
  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
    56
  val declare: Context.generic -> bool -> binding -> T -> string * T
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    57
  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
    58
  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
    59
  val change_ignore: 'a table -> 'a table
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    60
  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
    61
  val check_reports: Context.generic -> 'a table ->
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
    62
    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
    63
  val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    64
  val lookup_key: 'a table -> string -> (string * 'a) option
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
    65
  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
    66
  val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    67
  val alias_table: naming -> binding -> string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    68
  val hide_table: bool -> string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    69
  val del_table: string -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    70
  val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
    71
  val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    72
  val empty_table: string -> 'a table
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    73
  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
    74
  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
    75
    'a table * 'a table -> 'a table
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    76
  val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    77
  val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    78
  val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
    79
  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
    80
end;
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    81
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
    82
structure Name_Space: NAME_SPACE =
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    83
struct
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
    84
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    85
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    86
(** name spaces **)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
    87
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    88
(* datatype entry *)
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    89
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    90
type entry =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
    91
 {concealed: bool,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    92
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
    93
  theory_name: string,
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    94
  pos: Position.T,
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    95
  id: serial};
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
    96
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    97
fun entry_markup def kind (name, {pos, id, ...}: entry) =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49816
diff changeset
    98
  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
    99
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   100
fun print_entry_ref kind (name, entry) =
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   101
  quote (Markup.markup (entry_markup false kind (name, entry)) name);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   102
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   103
fun err_dup kind entry1 entry2 pos =
56038
0e2dec666152 tuned messages -- in accordance to Isabelle/Scala;
wenzelm
parents: 56025
diff changeset
   104
  error ("Duplicate " ^ plain_words kind ^ " declaration " ^
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   105
    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
   106
56038
0e2dec666152 tuned messages -- in accordance to Isabelle/Scala;
wenzelm
parents: 56025
diff changeset
   107
fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   108
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   109
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   110
(* datatype T *)
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   111
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   112
datatype T =
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33091
diff changeset
   113
  Name_Space of
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   114
   {kind: string,
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
   115
    internals: (string list * string list) Change_Table.T,  (*visible, hidden*)
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
   116
    entries: (xstring list * entry) Change_Table.T};        (*externals, entry*)
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   117
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   118
fun make_name_space (kind, internals, entries) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   119
  Name_Space {kind = kind, internals = internals, entries = entries};
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   120
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   121
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   122
  make_name_space (f (kind, internals, entries));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   123
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
   124
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
   125
  (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
   126
56139
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   127
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
   128
  (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
   129
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   130
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
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
   131
  (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   132
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   133
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
   134
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
   135
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   136
fun kind_of (Name_Space {kind, ...}) = kind;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   137
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
   138
fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
46869
26a9a4e0a631 more direct Name_Space.defined_entry;
wenzelm
parents: 45666
diff changeset
   139
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   140
fun the_entry (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
   141
  (case Change_Table.lookup entries name of
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
   142
    NONE => error (undefined kind name)
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   143
  | SOME (_, entry) => entry);
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   144
42487
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
   145
fun entry_ord space = int_ord o pairself (#id o the_entry space);
398d7d6bba42 export Name_Space.entry_ord;
wenzelm
parents: 42466
diff changeset
   146
42379
26f64dddf2c6 tuned signature;
wenzelm
parents: 42375
diff changeset
   147
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
   148
  (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
   149
    NONE => Markup.intensify
42135
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   150
  | SOME (_, entry) => entry_markup false kind (name, entry));
da200fa2768c decode_term: some context-sensitive markup;
wenzelm
parents: 41254
diff changeset
   151
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   152
fun is_concealed space name = #concealed (the_entry space name);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   153
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   154
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   155
(* name accesses *)
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   156
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   157
fun lookup (Name_Space {internals, ...}) xname =
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
   158
  (case Change_Table.lookup internals xname of
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   159
    NONE => (xname, true)
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   160
  | SOME ([], []) => (xname, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   161
  | SOME ([name], _) => (name, true)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   162
  | SOME (name :: _, _) => (name, false)
55669
4612c450b59c tuned signature;
wenzelm
parents: 53539
diff changeset
   163
  | SOME ([], name' :: _) => (Long_Name.hidden name', true));
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   164
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   165
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
   166
  (case Change_Table.lookup entries name of
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   167
    NONE => [name]
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   168
  | SOME (externals, _) => externals);
25072
03f57b516e12 store external accesses within name space (as produced by naming policy);
wenzelm
parents: 24361
diff changeset
   169
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   170
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
   171
  Change_Table.fold (fn (xname, (names, _)) =>
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   172
    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
   173
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   174
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   175
(* intern *)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   176
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   177
fun intern space xname = #1 (lookup space xname);
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   178
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   179
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   180
(* extern *)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   181
51949
f6858bb224c9 some system options as context-sensitive config options;
wenzelm
parents: 51510
diff changeset
   182
val names_long_raw = Config.declare_option "names_long";
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   183
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
   184
51949
f6858bb224c9 some system options as context-sensitive config options;
wenzelm
parents: 51510
diff changeset
   185
val names_short_raw = Config.declare_option "names_short";
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   186
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
   187
51949
f6858bb224c9 some system options as context-sensitive config options;
wenzelm
parents: 51510
diff changeset
   188
val names_unique_raw = Config.declare_option "names_unique";
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   189
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
   190
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42327
diff changeset
   191
fun extern ctxt space name =
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   192
  let
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   193
    val names_long = Config.get ctxt names_long;
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   194
    val names_short = Config.get ctxt names_short;
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   195
    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
   196
30277
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   197
    fun valid require_unique xname =
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   198
      let val (name', is_unique) = lookup space xname
4f2b6ccce047 adapted Binding.dest;
wenzelm
parents: 30242
diff changeset
   199
      in name = name' andalso (not require_unique orelse is_unique) end;
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   200
55669
4612c450b59c tuned signature;
wenzelm
parents: 53539
diff changeset
   201
    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
   202
      | 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
   203
  in
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   204
    if names_long then name
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42493
diff changeset
   205
    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
   206
    else ext (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   207
  end;
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   208
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   209
fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   210
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   211
fun extern_shortest ctxt =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   212
  extern
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   213
    (ctxt
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   214
      |> Config.put names_long false
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   215
      |> Config.put names_short false
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   216
      |> Config.put names_unique false);
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   217
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   218
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
   219
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
   220
51510
b4f7e6734acc tuned print_classes: more standard order, markup, formatting;
wenzelm
parents: 50301
diff changeset
   221
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   222
(* completion *)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   223
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   224
fun completion context space (xname, pos) =
55989
55827fc7c0dd ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
wenzelm
parents: 55977
diff changeset
   225
  if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   226
    let
56024
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   227
      fun result_ord ((s, _), (s', _)) =
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   228
        (case int_ord (pairself Long_Name.qualification (s, s')) of
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   229
          EQUAL => string_ord (s, s')
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   230
        | ord => ord);
55845
a05413276a0d allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
wenzelm
parents: 55840
diff changeset
   231
      val x = Name.clean xname;
55975
9962ca0875c9 no completion of concealed names;
wenzelm
parents: 55962
diff changeset
   232
      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
   233
      val ext = extern_shortest (Context.proof_of context) space;
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55672
diff changeset
   234
      val names =
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
   235
        Change_Table.fold
55975
9962ca0875c9 no completion of concealed names;
wenzelm
parents: 55962
diff changeset
   236
          (fn (a, (name :: _, _)) =>
9962ca0875c9 no completion of concealed names;
wenzelm
parents: 55962
diff changeset
   237
              if String.isPrefix x a andalso not (is_concealed space name)
56022
8c9ab5d91d5a more restrictive completion: intern/extern stability;
wenzelm
parents: 55989
diff changeset
   238
              then
8c9ab5d91d5a more restrictive completion: intern/extern stability;
wenzelm
parents: 55989
diff changeset
   239
                let val a' = ext name
8c9ab5d91d5a more restrictive completion: intern/extern stability;
wenzelm
parents: 55989
diff changeset
   240
                in if a = a' then cons (a', (kind, name)) else I end
8c9ab5d91d5a more restrictive completion: intern/extern stability;
wenzelm
parents: 55989
diff changeset
   241
              else I
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   242
            | _ => I) internals []
56024
0921c1dc344c more structured order;
wenzelm
parents: 56022
diff changeset
   243
        |> sort_distinct result_ord;
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
   244
    in Completion.names pos names end
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   245
  else Completion.none;
53539
51157ee7f5ba tuned signature;
wenzelm
parents: 51949
diff changeset
   246
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   247
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   248
(* modify internals *)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   249
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   250
val del_name = map_internals o apfst o remove (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   251
fun del_name_extra name =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   252
  map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   253
val add_name = map_internals o apfst o update (op =);
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   254
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
   255
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   256
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   257
(* hide *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   258
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   259
fun hide fully name space =
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   260
  if not (Long_Name.is_qualified name) then
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   261
    error ("Attempt to hide global name " ^ quote name)
55669
4612c450b59c tuned signature;
wenzelm
parents: 53539
diff changeset
   262
  else if Long_Name.is_hidden name then
8728
33a9643ba626 improved output of ambiguous entries;
wenzelm
parents: 6845
diff changeset
   263
    error ("Attempt to hide hidden name " ^ quote name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   264
  else
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   265
    let val names = valid_accesses space name in
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   266
      space
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   267
      |> add_name' name name
30359
3f9b3ff851ca moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   268
      |> fold (del_name name)
33049
c38f02fdf35d curried inter as canonical list operation (beware of argument order)
haftmann
parents: 33038
diff changeset
   269
        (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
   270
      |> fold (del_name_extra name) (get_accesses space name)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   271
    end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   272
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   273
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   274
(* merge *)
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   275
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   276
fun merge
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   277
  (Name_Space {kind = kind1, internals = internals1, entries = entries1},
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   278
    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
   279
  let
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   280
    val kind' =
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   281
      if kind1 = kind2 then kind1
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   282
      else error ("Attempt to merge different kinds of name spaces " ^
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   283
        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
   284
    val internals' = (internals1, internals2) |> Change_Table.join
30465
038839f111a1 renamed bind to define;
wenzelm
parents: 30438
diff changeset
   285
      (K (fn ((names1, names1'), (names2, names2')) =>
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   286
        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
   287
        then raise Change_Table.SAME
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   288
        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
   289
    val entries' = (entries1, entries2) |> Change_Table.join
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   290
      (fn name => fn ((_, entry1), (_, entry2)) =>
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
   291
        if #id entry1 = #id entry2 then raise Change_Table.SAME
49816
e63d6c55ad6d more position information for hyperlink and placement of message;
wenzelm
parents: 49528
diff changeset
   292
        else err_dup kind' (name, entry1) (name, entry2) Position.none);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   293
  in make_name_space (kind', internals', entries') end;
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   294
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   295
26440
feeb83f9657f tuned comments;
wenzelm
parents: 25225
diff changeset
   296
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   297
(** naming context **)
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   298
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   299
(* datatype naming *)
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   300
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   301
datatype naming = Naming of
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   302
 {conceal: bool,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   303
  group: serial option,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   304
  theory_name: string,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   305
  path: (string * bool) list};
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   306
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   307
fun make_naming (conceal, group, theory_name, path) =
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   308
  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
   309
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   310
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
   311
  make_naming (f (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   312
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   313
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
   314
  (conceal, group, theory_name, f path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   315
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   316
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   317
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
   318
  (true, group, theory_name, path));
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   319
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   320
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
   321
  (conceal, group, theory_name, path));
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   322
33724
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   323
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   324
fun get_group (Naming {group, ...}) = group;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   325
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   326
fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   327
  (conceal, group, theory_name, path));
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   328
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   329
fun new_group naming = set_group (SOME (serial ())) naming;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   330
val reset_group = set_group NONE;
5ee13e0428d2 uniform new_group/reset_group;
wenzelm
parents: 33281
diff changeset
   331
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   332
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
   333
val root_path = map_path (fn _ => []);
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   334
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
   335
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
   336
35200
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   337
fun qualified_path mandatory binding = map_path (fn path =>
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   338
  path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
aaddb2b526d6 more systematic treatment of qualified names derived from binding;
wenzelm
parents: 33724
diff changeset
   339
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   340
val default_naming = make_naming (false, NONE, "", []);
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   341
val local_naming = default_naming |> add_path "local";
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   342
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   343
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   344
(* full name *)
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   345
41254
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 35679
diff changeset
   346
fun err_bad binding = error (Binding.bad binding);
78c3e472bb35 extra checking of name bindings for classes, types, consts;
wenzelm
parents: 35679
diff changeset
   347
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   348
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
   349
  | transform_binding _ = I;
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   350
55962
fbd0e768bc8f special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
wenzelm
parents: 55961
diff changeset
   351
val bad_specs = ["", "??", "__"];
fbd0e768bc8f special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
wenzelm
parents: 55961
diff changeset
   352
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   353
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
   354
  let
33281
223ef9bc399a let naming transform binding beforehand -- covering only the "conceal" flag for now;
wenzelm
parents: 33164
diff changeset
   355
    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
   356
    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
   357
    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
   358
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   359
    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
   360
    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
   361
    val spec = spec1 @ spec2;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   362
    val _ =
55962
fbd0e768bc8f special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
wenzelm
parents: 55961
diff changeset
   363
      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   364
      andalso err_bad binding;
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   365
  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
   366
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   367
fun full_name naming =
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   368
  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
   369
47021
f35f654f297d clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents: 47005
diff changeset
   370
val base_name = full_name default_naming #> Long_Name.base_name;
f35f654f297d clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
wenzelm
parents: 47005
diff changeset
   371
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   372
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   373
(* accesses *)
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   374
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   375
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
   376
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   377
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
   378
and mandatory_prefixes1 [] = []
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   379
  | 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
   380
  | 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
   381
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   382
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
   383
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   384
fun accesses naming binding =
30412
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   385
  let
33157
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   386
    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
   387
    val sfxs = mandatory_suffixes spec;
7f5b0a020ccd just one naming policy based on binding content -- eliminated odd "object-oriented" style;
wenzelm
parents: 30359
diff changeset
   388
    val pfxs = mandatory_prefixes spec;
30522
e26b80647189 removed obsolete no_base_names naming policy;
wenzelm
parents: 30469
diff changeset
   389
  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
   390
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   391
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   392
(* alias *)
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   393
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   394
fun alias naming binding name space =
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   395
  let
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   396
    val (accs, accs') = accesses naming binding;
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   397
    val space' = space
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   398
      |> fold (add_name name) accs
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   399
      |> map_name_space (fn (kind, internals, entries) =>
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   400
        let
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
   401
          val _ = Change_Table.defined entries name orelse error (undefined kind name);
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   402
          val entries' = entries
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
   403
            |> Change_Table.map_entry name (fn (externals, entry) =>
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   404
              (Library.merge (op =) (externals, accs'), entry))
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   405
        in (kind, internals, entries') end);
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   406
  in space' end;
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   407
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   408
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   409
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   410
(** context naming **)
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   411
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   412
structure Data_Args =
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   413
struct
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   414
  type T = naming;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   415
  val empty = default_naming;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   416
  fun extend _ = default_naming;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   417
  fun merge _ = default_naming;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   418
  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
   419
end;
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   420
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   421
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
   422
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
   423
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   424
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
   425
  | 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
   426
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   427
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
   428
  | 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
   429
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
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   432
(** entry definition **)
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   433
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   434
(* declaration *)
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   435
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   436
fun new_entry strict (name, (externals, entry)) =
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   437
  map_name_space (fn (kind, internals, entries) =>
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   438
    let
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   439
      val entries' =
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
   440
        (if strict then Change_Table.update_new else Change_Table.update)
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
   441
          (name, (externals, entry)) 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
   442
        handle Change_Table.DUP dup =>
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
   443
          err_dup kind (dup, #2 (the (Change_Table.lookup entries dup))) (name, entry) (#pos entry);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   444
    in (kind, internals, entries') end);
33091
d23e75d4f7da maintain abstract entry, with position, identity etc.;
wenzelm
parents: 33049
diff changeset
   445
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   446
fun declare context strict binding space =
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   447
  let
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   448
    val naming = naming_of context;
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   449
    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
   450
    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
   451
    val (accs, accs') = accesses naming binding;
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   452
56f836b9414f allow name space entries to be "concealed" -- via binding/naming/local_theory;
wenzelm
parents: 33097
diff changeset
   453
    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
   454
    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
   455
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 49358
diff changeset
   456
    val (proper_pos, pos) = Position.default (Binding.pos_of binding);
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   457
    val entry =
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   458
     {concealed = concealed,
33164
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   459
      group = group,
b8fd9b6bba7c Name_Space.naming: maintain group and theory_name as well;
wenzelm
parents: 33157
diff changeset
   460
      theory_name = theory_name,
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42358
diff changeset
   461
      pos = pos,
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   462
      id = serial ()};
35679
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   463
    val space' = space
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   464
      |> fold (add_name name) accs
da87ffdcf7ea added Name_Space.alias -- additional accesses for an existing entry;
wenzelm
parents: 35432
diff changeset
   465
      |> new_entry strict (name, (accs', entry));
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 47003
diff changeset
   466
    val _ =
56160
d348378ddf47 tuned -- avoid vacuous reports;
wenzelm
parents: 56139
diff changeset
   467
      if proper_pos andalso Context_Position.is_reported_generic context pos then
d348378ddf47 tuned -- avoid vacuous reports;
wenzelm
parents: 56139
diff changeset
   468
        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
   469
      else ();
30233
6eb726e43ed1 eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm
parents: 30222
diff changeset
   470
  in (name, space') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   471
16137
00e9ca1e7261 renamed cond_extern to extern;
wenzelm
parents: 16002
diff changeset
   472
47003
3094745a41ef tuned structure;
wenzelm
parents: 46869
diff changeset
   473
(* definition in symbol table *)
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   474
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
   475
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
   476
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
   477
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
   478
  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
   479
56139
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   480
fun change_ignore (Table (space, tab)) =
b7add947a6ef more frugal recording of changes: join merely requires information from one side;
wenzelm
parents: 56056
diff changeset
   481
  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
   482
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   483
fun space_of_table (Table (space, _)) = space;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   484
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   485
fun check_reports context (Table (space, tab)) (xname, ps) =
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   486
  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
   487
    (case Change_Table.lookup tab name of
55696
de2668c50403 tuned whitespace;
wenzelm
parents: 55694
diff changeset
   488
      SOME x =>
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   489
        let
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   490
          val reports =
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   491
            filter (Context_Position.is_reported_generic context) ps
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   492
            |> 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
   493
        in ((name, reports), x) end
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55669
diff changeset
   494
    | NONE =>
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   495
        let
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   496
          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
   497
        in
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   498
          error (undefined (kind_of 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
   499
            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
   500
        end)
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   501
  end;
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   502
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   503
fun check context table (xname, pos) =
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   504
  let
55956
94d384d621b0 reject internal term names outright, and complete consts instead;
wenzelm
parents: 55923
diff changeset
   505
    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
   506
    val _ = Position.reports reports;
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   507
  in (name, x) end;
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55845
diff changeset
   508
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
   509
fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   510
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   511
fun get table name =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   512
  (case lookup_key table name of
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   513
    SOME (_, x) => x
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   514
  | NONE => error (undefined (kind_of (space_of_table table)) name));
42466
bbce02fcba60 added Name_Space.check/get convenience;
wenzelm
parents: 42379
diff changeset
   515
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   516
fun define context strict (binding, x) (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   517
  let
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   518
    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
   519
    val tab' = Change_Table.update (name, x) tab;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   520
  in (name, Table (space', tab')) end;
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   521
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   522
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   523
(* derived table operations *)
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   524
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   525
fun alias_table naming binding name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   526
  Table (alias naming binding name space, tab);
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   527
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   528
fun hide_table fully name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   529
  Table (hide fully name space, tab);
16341
e573e5167eda added type NameSpace.table with basic operations;
wenzelm
parents: 16262
diff changeset
   530
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   531
fun del_table name (Table (space, tab)) =
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   532
  let
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   533
    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
   534
    val tab' = Change_Table.delete_safe name tab;
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   535
  in Table (space', tab') end;
28860
b1d46059d502 name spaces and name bindings
haftmann
parents: 27196
diff changeset
   536
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   537
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
   538
  Table (space, Change_Table.map_entry name f tab);
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   539
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
   540
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
   541
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
   542
fun empty_table kind = Table (empty kind, Change_Table.empty);
56025
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 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
   545
  Table (merge (space1, space2), Change_Table.merge (K true) (tab1, tab2));
28991
694227dd3e8c dropped NameSpace.declare_base
haftmann
parents: 28965
diff changeset
   546
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   547
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
   548
  Table (merge (space1, space2), Change_Table.join f (tab1, tab2));
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   549
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   550
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   551
(* present table content *)
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   552
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   553
fun extern_entries ctxt space entries =
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   554
  fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
16848
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   555
  |> Library.sort_wrt (#2 o #1);
1c8a5bb7c688 added dest_table;
wenzelm
parents: 16444
diff changeset
   556
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   557
fun markup_entries ctxt space entries =
4873054cd1fc tuned signature;
wenzelm
parents: 56038
diff changeset
   558
  extern_entries ctxt space entries
56025
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
diff changeset
   559
  |> map (fn ((name, xname), x) => ((markup space name, xname), x));
d74fed45fa8b abstract type Name_Space.table;
wenzelm
parents: 56024
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 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
   562
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
   563
5012
086b055c4d73 moved name_space.ML to General/name_space.ML;
wenzelm
parents:
diff changeset
   564
end;
30215
47cce3d47e62 moved name space externalization flags back to name_space.ML;
wenzelm
parents: 30213
diff changeset
   565