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