src/Pure/Isar/proof_context.ML
2011-11-27 wenzelm 2011-11-27 tuned;
2011-11-11 wenzelm 2011-11-11 more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
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-11-03 wenzelm 2011-11-03 more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;
2011-11-03 wenzelm 2011-11-03 tuned signature -- canonical argument order;
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-25 wenzelm 2011-06-25 entity markup for "type", "constant";
2011-06-25 wenzelm 2011-06-25 type classes: entity markup instead of old-style token markup;
2011-05-12 wenzelm 2011-05-12 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;
2011-04-28 wenzelm 2011-04-28 literal facts `prop` may contain dummy patterns;
2011-04-28 wenzelm 2011-04-28 eliminated slightly odd Proof_Context.bind_fixes; tuned;
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 more precise position information via Variable.add_fixes_binding;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-23 wenzelm 2011-04-23 clarified Consts.read_const;
2011-04-23 wenzelm 2011-04-23 clarified Type.the_decl;
2011-04-23 wenzelm 2011-04-23 more reports and error positions;
2011-04-19 wenzelm 2011-04-19 split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
2011-04-19 wenzelm 2011-04-19 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;
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 tuned signature;
2011-04-17 wenzelm 2011-04-17 markup facts via name space; eliminated obsolete markup;
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 do not open ML structures;
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-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
2011-04-08 wenzelm 2011-04-08 moved CONST syntax/translations to their proper place;
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 Mixfix; eliminated slightly odd no_syn convenience;
2011-04-07 wenzelm 2011-04-07 simplified printer context: uniform externing and static token translations;
2011-04-06 wenzelm 2011-04-06 eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;
2011-04-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-04-05 wenzelm 2011-04-05 separate module for standard implementation of inner syntax operations;
2011-04-05 wenzelm 2011-04-05 discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05 wenzelm 2011-04-05 more precise propagation of reports/results through some inner syntax layers; misc reorganization;
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;
2011-03-30 wenzelm 2011-03-30 accomodate autofix discipline of non-body context;
2011-03-30 wenzelm 2011-03-30 more informative markup_free;
2011-03-27 wenzelm 2011-03-27 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;
2011-03-27 wenzelm 2011-03-27 tuned signatures;
2011-03-27 wenzelm 2011-03-27 decode_term/disambig: report resolved term variables for the unique (!) result;
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-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17 wenzelm 2010-09-17 tuned signature of (Context_)Position.report variants;
2010-09-17 wenzelm 2010-09-17 allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-13 wenzelm 2010-09-13 tuned signature; tuned comments;
2010-09-13 wenzelm 2010-09-13 Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;
2010-09-12 wenzelm 2010-09-12 Type_Infer.infer_types: plain error instead of kernel exception TYPE;
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 eliminated aliases of Type.constraint;
2010-09-07 wenzelm 2010-09-07 highlight bad range of nested error (here from inner parsing);