23 months ago wenzelm 2017-07-03 unused;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 support private scope for individual local theory commands; tuned signature;
2015-04-01 wenzelm 2015-04-01 tuned signature;
2015-03-31 wenzelm 2015-03-31 support for explicit scope of private entries;
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2015-03-29 wenzelm 2015-03-29 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-21 wenzelm 2014-03-21 tuned signature;
2014-03-12 wenzelm 2014-03-12 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
2014-03-11 wenzelm 2014-03-11 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;
2014-03-10 wenzelm 2014-03-10 tuned signature -- prefer Name_Space.get with its builtin error;
2014-03-10 wenzelm 2014-03-10 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;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2012-03-18 wenzelm 2012-03-18 comment;
2012-03-18 wenzelm 2012-03-18 tuned;
2012-03-18 wenzelm 2012-03-18 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;
2011-11-25 wenzelm 2011-11-25 prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;
2011-11-09 wenzelm 2011-11-09 sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;
2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-18 wenzelm 2011-04-18 standardized aliases of operations on tsig;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 simplified Pure syntax bootstrap;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-07 wenzelm 2011-04-07 discontinued user-defined token translations; tuned signature;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-03 wenzelm 2011-04-03 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;
2010-12-04 wenzelm 2010-12-04 added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_) variants;
2010-09-12 wenzelm 2010-09-12 load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
2010-09-12 wenzelm 2010-09-12 common Type.appl_error, which also covers explicit constraints;
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 modernized/simplified Sign.set_defsort;
2010-04-16 wenzelm 2010-04-16 replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;
2010-04-15 wenzelm 2010-04-15 misc tuning and simplification;
2010-03-27 wenzelm 2010-03-27 disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-15 wenzelm 2010-03-15 tuned;
2010-03-15 wenzelm 2010-03-15 moved old Sign.intern_term to the place where it is still used;
2010-03-09 wenzelm 2010-03-09 aliases for class/type/const; tuned;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-03-03 wenzelm 2010-03-03 authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;