src/Pure/Isar/proof_context.ML
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);
2010-09-06 wenzelm 2010-09-06 discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.;
2010-09-05 wenzelm 2010-09-05 Syntax.standard_parse_term: eliminated redundant Pretty.pp;
2010-09-02 wenzelm 2010-09-02 inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-09-01 wenzelm 2010-09-01 prefer regular print functions over slightly low-level Term.string_of_vname;
2010-08-26 wenzelm 2010-08-26 renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-11 wenzelm 2010-08-11 tuned whitespace;
2010-08-08 wenzelm 2010-08-08 proper context for Syntax.parse_token;
2010-08-08 wenzelm 2010-08-08 prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
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-29 wenzelm 2010-04-29 read_const: disallow internal names as usual in visible Isar text;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-29 wenzelm 2010-04-29 allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-28 wenzelm 2010-04-28 localized default sort;
2010-04-28 wenzelm 2010-04-28 more systematic naming of tsig operations;
2010-04-28 wenzelm 2010-04-28 get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;
2010-04-27 wenzelm 2010-04-27 monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-15 wenzelm 2010-04-15 get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;
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-06 wenzelm 2010-03-06 provide ProofContext.def_type depending on "pattern" mode;
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;
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2010-02-27 wenzelm 2010-02-27 clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-25 wenzelm 2010-02-25 clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-21 wenzelm 2010-02-21 slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm 2010-02-21 authentic syntax for *all* term constants;
2010-02-18 berghofe 2010-02-18 Use top-down rewriting to contract abbreviations.