clarified signature: store full theory name;

clarified signature;

clarified signature: more types;

clarified signature;

proper completion for @{named_theorems};

more operations;

complete on long name components as well;

tuned;

more symbols;

replaced inefficient valid_accesses by is_valid_access, based on stored input accesses: e.g. relevant for Proof_Context.update_thms;

less redundant exploration of full name space;

tuned;

clarified signature;

highlighting of entity def/ref positions wrt. cursor;

more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);

tuned signature;
tuned;

tuned signature, in accordance to sortBy in Scala;

clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";

more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

support for 'restricted' modifier: only qualified accesses outside the local scope;

tuned message;

support private scope for individual local theory commands;
tuned signature;

more uniform "verbose" option to print name space;

export for informative purposes;

tuned message;

tuned signature;

more visibility flags on background naming;

support for explicit scope of private entries;

subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;

tuned signature;

tuned signature;

tuned;

tuned signature;

tuned signature;

support for strictly private name space entries;
tuned signature;

semantic completion for @{system_option};

renamed "pairself" to "apply2", in accordance to @{apply 2};

tuned signature;

clarified signature: entity serial number is not position id;

more source positions;

more uniform alias vs. hide: proper check, allow to hide global names as well;

minor tuning;

clarified completion ordering: prefer local names;

tuned -- avoid vacuous reports;

more frugal recording of changes: join merely requires information from one side;
tuned;

more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;

tuned signature;

tuned messages -- in accordance to Isabelle/Scala;

abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

more structured order;

more restrictive completion: intern/extern stability;

ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");

more detailed description of completion items;

no completion of concealed names;

special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;

completion is part of error (not report) and thus not subject to context visibility -- e.g. relevant for 'fixes' in long statements;

more compact Markup.markup_report: message body may consist of multiple elements;

reject internal term names outright, and complete consts instead;
more general Name_Space.check_reports;
more compact Markup.markup_report;

tuned;

more markup for inner syntax class/type names (notably for completion);
explicit reports result without broadcast yet, which is important for brute-force disambiguation;

allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;

consider completion report as part of error message -- less stateful, may get handled;

modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
removed obsolete Method.Source_i;
proper context for global data;
tuned messages;

tuned whitespace;

clarified semantic completion: retain kind.full_name as official item name for history;
misc tuning;

clarified completion names;
tuned signature;

support for completion within the formal context;
tuned signature;

tuned signature;

tuned signature;

some system options as context-sensitive config options;

tuned print_classes: more standard order, markup, formatting;
uniform printing of minimal supersort/classrel;

print formal entities with markup;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

more position information for hyperlink and placement of message;

report proper binding positions only -- avoid swamping document model with unspecific information;

clarified markup names;

renamed Position.str_of to Position.here;

clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

tuned structure;

more direct Name_Space.defined_entry;
tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

entity markup for bound variables;

ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

more conventional naming scheme: names_long, names_short, names_unique;

more informative markup for fixed variables (via name space entry);
uniform markup for undeclared entities;
tuned;

export Name_Space.entry_ord;

added Name_Space.check/get convenience;

tuned signature;

report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

Name_Space.entry_markup: keep def position as separate properties;
uniform treatment of ML_def/ML_open/ML_struct as entities;
hyperlinks for all entities -- excluding ML_open/ML_struct for now;

decode_term: some context-sensitive markup;
more informative Markup.entity and Name_Space.markup_entry;
Markup.const: use "constant" to make it coincide with name space kind;

extra checking of name bindings for classes, types, consts;
tuned;

added Name_Space.alias -- additional accesses for an existing entry;

removed unused external_names;

more systematic treatment of qualified names derived from binding;

uniform new_group/reset_group;
tuned signature;

let naming transform binding beforehand -- covering only the "conceal" flag for now;
export LocalTheory.standard_morphism;

Name_Space.naming: maintain group and theory_name as well;
tuned;

allow name space entries to be "concealed" -- via binding/naming/local_theory;

maintain position of formal entities via name space;

maintain explicit name space kind;
export Name_Space.the_entry;
tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

maintain abstract entry, with position, identity etc.;
declare/define: explicit indication of strictness;
merge_tables/join_tables: disallow duplicates based on entry identity;

curried inter as canonical list operation (beware of argument order)

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

explicit indication of Unsynchronized.ref;

removed obsolete no_base_names naming policy;

renamed sticky_prefix to mandatory_path;

renamed bind to define;
misc tuning and polishing;

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);

add_path: discontinued special meaning of "//", "/", "..";
added root_path, parent_path;

just one naming policy based on binding content -- eliminated odd "object-oriented" style;
uniform handling of regular vs. mandatory name prefixes -- add_path and sticky_prefix may be freely intermixed;
misc tuning and cleanup;

moved basic algebra of long names from structure NameSpace to Long_Name;
tuned signature;

renamed NameSpace.base to NameSpace.base_name;
renamed NameSpace.map_base to NameSpace.map_base_name;
eliminated alias Sign.base_name = NameSpace.base_name;

adapted Binding.dest;
tuned;

Merge.

eliminated internal stamp equality, replaced by bare-metal pointer_eq;
misc tuning and polishing;

moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;

moved name space externalization flags back to name_space.ML;
added pure version extern_flags;
do not export internal get_accesses;

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);

Nicer names in FindTheorems.
* Patch NameSpace.get_accesses, contributed by Timothy Bourke:

NameSpace.get_accesses has been patched to fix the following
bug:
theory OverHOL imports Main begin
lemma conjI: "a & b --> b"
by blast

ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of;
val x1 = NameSpace.get_accesses ns "HOL.conjI";
val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *}
end

where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"],
but x1 should be just ["HOL.conjI"].

NameSpace.get_accesses is only used within the NameSpace
structure itself. The two uses have been modified to retain
their original behaviour.

Note that NameSpace.valid_accesses gives different results:
get_accesses ns "HOL.eq_class.eq"
gives ["eq", "eq_class.eq", "HOL.eq_class.eq"]
but,
valid_accesses ns "HOL.eq_class.eq"
gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"]

* Patch FindTheorems:
Prefer names that are shorter to type in the current context.

* Re-export space_of.

binding is alias for Binding.T

separator, is_qualified

removed Table.extend, NameSpace.extend_table

dropped NameSpace.declare_base

cleaned up binding module and related code

new Binding module

exported get_accesses (for diagnostic purpose)

name spaces and name bindings

hide: delete all accesses from extra names -- reduces ambiguity in extern;

merge: canonical order;

tuned comments;
tuned;

export is_hidden;

store external accesses within name space (as produced by naming policy);
improved sticky_prefix: suppress redundant accesses to achieve shorter output;
removed unused interfaces;
replaced accesses' by external_names (depening on naming);

tuned signature;

declare: disallow quote (") in names;

tuned Pure/General/name_space.ML

removed NameSpace.split -- use qualifier/base instead;

removed conditional combinator;

added split

avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;

renamed NameSpace.drop_base to NameSpace.qualifier;

tuned;

avoid polymorphic equality;

removed qualified_force_prefix;
added sticky_prefix;

low-level tuning of merge: maintain identity of accesses;
simplified TableFun.join;

removed custom_accesses;
added suffixes_prefixes_split, qualified_force_prefix;

tuned;

cleaned up nth, nth_update, nth_map and nth_string functions

minor tweaks for Poplog/ML;

TableFun/Symtab: curried lookup and update;

curried_lookup/update;

removed unused dest operation;

added dest_table;

Symtab.fold;

added type NameSpace.table with basic operations;

no warning for non-identifiers;

renamed cond_extern to extern;
append, base, drop_base, map_base: made robust against empty names;
added qualified;
extern: improved output for non-unique non-hidden names;
name entry path superceded by general naming context;
added reject_qualified, default_naming, add_path, no_base_names, custom_accesses, set_policy;

tuned;

Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

added flag unique_names

Merged in license change from Isabelle2004

Added flag short_names

Modified merge_aux to prevent newer names from getting overwritten
by older names.

added accesses';

hide: flag for full/base name;

moved prefixes1, suffixes1 to library.ML;

added map_base;

export hidden: string -> string;

GPLed;

improved output of ambiguous entries;
support hiding;

added cond_extern_table;

fixed titles;

Symtab.foldl;

moved long_names / cond_extern to name_space.ML;

moved name_space.ML to General/name_space.ML;