author  wenzelm 
Sat, 15 Mar 2014 11:57:55 +0100  
changeset 56160  d348378ddf47 
parent 56139  b7add947a6ef 
child 56162  ea6303e2261b 
permissions  rwrr 
6118  1 
(* Title: Pure/General/name_space.ML 
5012  2 
Author: Markus Wenzel, TU Muenchen 
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  6 
*) 
7 

26440  8 
type xstring = string; (*external names*) 
5012  9 

10 
signature NAME_SPACE = 

11 
sig 

12 
type T 

33096  13 
val empty: string > T 
14 
val kind_of: T > string 

46869  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  18 
val entry_ord: T > string * string > order 
42379  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  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  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  34 
val hide: bool > string > T > T 
5012  35 
val merge: T * T > T 
16137  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  38 
val get_group: naming > serial option 
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  41 
val new_group: naming > naming 
42 
val reset_group: naming > naming 

16137  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  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  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  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 speedup 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  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  64 
val lookup_key: 'a table > string > (string * 'a) option 
42466  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  67 
val alias_table: naming > binding > string > 'a table > 'a table 
68 
val hide_table: bool > string > 'a table > 'a table 

69 
val del_table: string > 'a table > 'a table 

70 
val map_table_entry: string > ('a > 'a) > 'a table > 'a table 

71 
val fold_table: (string * 'a > 'b > 'b) > 'a table > 'b > 'b 

33096  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 speedup 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  76 
val extern_entries: Proof.context > T > (string * 'a) list > ((string * xstring) * 'a) list 
77 
val markup_entries: Proof.context > T > (string * 'a) list > ((Markup.T * xstring) * 'a) list 

78 
val extern_table: Proof.context > 'a table > ((string * xstring) * 'a) list 

79 
val markup_table: Proof.context > 'a table > ((Markup.T * xstring) * 'a) list 

5012  80 
end; 
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  83 
struct 
84 

30412
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

85 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

86 
(** name spaces **) 
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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  97 
fun entry_markup def kind (name, {pos, id, ...}: entry) = 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract 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  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  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  108 

33091
d23e75d4f7da
maintain abstract entry, with position, identity etc.;
wenzelm
parents:
33049
diff
changeset

109 

5012  110 
(* datatype T *) 
111 

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  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 speedup 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 speedup 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  117 

118 
fun make_name_space (kind, internals, entries) = 

119 
Name_Space {kind = kind, internals = internals, entries = entries}; 

120 

121 
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) = 

122 
make_name_space (f (kind, internals, entries)); 

123 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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 speedup 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 speedup 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  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 speedup 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  132 

5012  133 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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  135 

136 
fun kind_of (Name_Space {kind, ...}) = kind; 

5012  137 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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  139 

33096  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 speedup 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  145 
fun entry_ord space = int_ord o pairself (#id o the_entry space); 
146 

42379  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 speedup 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
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49816
diff
changeset

149 
NONE => Markup.intensify 
42135  150 
 SOME (_, entry) => entry_markup false kind (name, entry)); 
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  153 

154 

155 
(* name accesses *) 

156 

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 speedup 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  159 
NONE => (xname, true) 
30233
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

160 
 SOME ([], []) => (xname, true) 
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

161 
 SOME ([name], _) => (name, true) 
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

162 
 SOME (name :: _, _) => (name, false) 
55669  163 
 SOME ([], name' :: _) => (Long_Name.hidden name', true)); 
8728  164 

33096  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 speedup 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  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 speedup Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents:
56052
diff
changeset

171 
Change_Table.fold (fn (xname, (names, _)) => 
33096  172 
if not (null names) andalso hd names = name then cons xname else I) internals []; 
8728  173 

174 

55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55669
diff
changeset

175 
(* intern *) 
16137  176 

177 
fun intern space xname = #1 (lookup space xname); 

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 contextsensitive 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 contextsensitive 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 contextsensitive 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  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  197 
fun valid require_unique xname = 
198 
let val (name', is_unique) = lookup space xname 

199 
in name = name' andalso (not require_unique orelse is_unique) end; 

8728  200 

55669  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  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  207 
end; 
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 sublanguages (main wildcard 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  227 
fun result_ord ((s, _), (s', _)) = 
228 
(case int_ord (pairself Long_Name.qualification (s, s')) of 

229 
EQUAL => string_ord (s, s') 

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  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  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 speedup Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents:
56052
diff
changeset

235 
Change_Table.fold 
55975  236 
(fn (a, (name :: _, _)) => 
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  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  246 

5012  247 

33096  248 
(* modify internals *) 
16137  249 

33096  250 
val del_name = map_internals o apfst o remove (op =); 
251 
fun del_name_extra name = 

252 
map_internals (apfst (fn [] => []  x :: xs => x :: remove (op =) name xs)); 

253 
val add_name = map_internals o apfst o update (op =); 

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  256 

257 
(* hide *) 

5012  258 

16137  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  261 
error ("Attempt to hide global name " ^ quote name) 
55669  262 
else if Long_Name.is_hidden name then 
8728  263 
error ("Attempt to hide hidden name " ^ quote name) 
16137  264 
else 
265 
let val names = valid_accesses space name in 

266 
space 

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  271 
end; 
5012  272 

273 

16137  274 
(* merge *) 
5012  275 

33096  276 
fun merge 
277 
(Name_Space {kind = kind1, internals = internals1, entries = entries1}, 

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  280 
val kind' = 
281 
if kind1 = kind2 then kind1 

282 
else error ("Attempt to merge different kinds of name spaces " ^ 

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 speedup 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  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 speedup 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 baremetal 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 speedup 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 speedup 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  293 
in make_name_space (kind', internals', entries') end; 
5012  294 

16137  295 

26440  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  298 

299 
(* datatype naming *) 

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  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  322 

33724  323 

324 
fun get_group (Naming {group, ...}) = group; 

325 

326 
fun set_group group = map_naming (fn (conceal, _, theory_name, path) => 

327 
(conceal, group, theory_name, path)); 

328 

329 
fun new_group naming = set_group (SOME (serial ())) naming; 

330 
val reset_group = set_group NONE; 

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  343 

30233
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

344 
(* full name *) 
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal 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 wildcard for completion;
wenzelm
parents:
55961
diff
changeset

351 
val bad_specs = ["", "??", "__"]; 
fbd0e768bc8f
special identifier "__" (i.e. empty name with internal suffix) serves as wildcard 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 baremetal 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: userlevel 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

358 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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: userlevel 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

361 
val spec = spec1 @ spec2; 
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

362 
val _ = 
55962
fbd0e768bc8f
special identifier "__" (i.e. empty name with internal suffix) serves as wildcard 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 "objectoriented" 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 "objectoriented" 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 "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

372 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

373 
(* accesses *) 
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

374 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

376 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

378 
and mandatory_prefixes1 [] = [] 
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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 "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

381 

7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

383 

30522  384 
fun accesses naming binding = 
30412
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" 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 "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

387 
val sfxs = mandatory_suffixes spec; 
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

388 
val pfxs = mandatory_prefixes spec; 
30522  389 
in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end; 
30412
7f5b0a020ccd
just one naming policy based on binding content  eliminated odd "objectoriented" style;
wenzelm
parents:
30359
diff
changeset

390 

30233
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

391 

47003  392 
(* alias *) 
393 

394 
fun alias naming binding name space = 

395 
let 

396 
val (accs, accs') = accesses naming binding; 

397 
val space' = space 

398 
> fold (add_name name) accs 

399 
> map_name_space (fn (kind, internals, entries) => 

400 
let 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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  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 speedup 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  404 
(Library.merge (op =) (externals, accs'), entry)) 
405 
in (kind, internals, entries') end); 

406 
in space' end; 

407 

408 

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  432 
(** entry definition **) 
433 

30233
6eb726e43ed1
eliminated internal stamp equality, replaced by baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

434 
(* declaration *) 
28860  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  437 
map_name_space (fn (kind, internals, entries) => 
438 
let 

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 speedup 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 speedup 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 speedup 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 speedup 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  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 baremetal 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 "objectoriented" 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  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  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  467 
if proper_pos andalso Context_Position.is_reported_generic context pos then 
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 baremetal pointer_eq;
wenzelm
parents:
30222
diff
changeset

470 
in (name, space') end; 
28860  471 

16137  472 

47003  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 speedup 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 speedup 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 speedup 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 speedup 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  483 
fun space_of_table (Table (space, _)) = space; 
484 

485 
fun check_reports context (Table (space, tab)) (xname, ps) = 

42466  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 speedup 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  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  501 
end; 
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 speedup 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  510 

511 
fun get table name = 

512 
(case lookup_key table name of 

513 
SOME (_, x) => x 

514 
 NONE => error (undefined (kind_of (space_of_table table)) name)); 

42466  515 

56025  516 
fun define context strict (binding, x) (Table (space, tab)) = 
517 
let 

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 speedup 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  520 
in (name, Table (space', tab')) end; 
521 

522 

523 
(* derived table operations *) 

524 

525 
fun alias_table naming binding name (Table (space, tab)) = 

526 
Table (alias naming binding name space, tab); 

527 

528 
fun hide_table fully name (Table (space, tab)) = 

529 
Table (hide fully name space, tab); 

16341
e573e5167eda
added type NameSpace.table with basic operations;
wenzelm
parents:
16262
diff
changeset

530 

56025  531 
fun del_table name (Table (space, tab)) = 
532 
let 

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 speedup 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  535 
in Table (space', tab') end; 
28860  536 

56025  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 speedup 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  539 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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 speedup 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  543 

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 speedup 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  546 

56025  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 speedup 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  549 

550 

551 
(* present table content *) 

552 

56052  553 
fun extern_entries ctxt space entries = 
554 
fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries [] 

16848  555 
> Library.sort_wrt (#2 o #1); 
556 

56052  557 
fun markup_entries ctxt space entries = 
558 
extern_entries ctxt space entries 

56025  559 
> map (fn ((name, xname), x) => ((markup space name, xname), x)); 
560 

56056
4d46d53566e6
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speedup 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 speedup 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  564 
end; 
30215
47cce3d47e62
moved name space externalization flags back to name_space.ML;
wenzelm
parents:
30213
diff
changeset

565 