| 2012-03-18 |
wenzelm |
2012-03-18 |
comment;
|
file | diff | annotate |
| 2012-03-18 |
wenzelm |
2012-03-18 |
tuned;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2011-06-08 |
wenzelm |
2011-06-08 |
more robust exception pattern General.Subscript;
|
file | diff | annotate |
| 2011-04-18 |
wenzelm |
2011-04-18 |
standardized aliases of operations on tsig;
|
file | diff | annotate |
| 2011-04-18 |
wenzelm |
2011-04-18 |
pass plain Proof.context for pretty printing;
|
file | diff | annotate |
| 2011-04-18 |
wenzelm |
2011-04-18 |
simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;
|
file | diff | annotate |
| 2011-04-17 |
wenzelm |
2011-04-17 |
added Binding.print convenience, which includes quote already;
|
file | diff | annotate |
| 2011-04-17 |
wenzelm |
2011-04-17 |
eliminated obsolete markup -- superseded by generic "entity" markup;
|
file | diff | annotate |
| 2011-04-17 |
wenzelm |
2011-04-17 |
report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
modernized structure Proof_Context;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
prefer local name spaces;
tuned signatures;
tuned;
|
file | diff | annotate |
| 2011-04-16 |
wenzelm |
2011-04-16 |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
simplified Pure syntax bootstrap;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
discontinued special treatment of structure Lexicon;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
clarified Syntax.root;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
|
file | diff | annotate |
| 2011-04-07 |
wenzelm |
2011-04-07 |
discontinued user-defined token translations;
tuned signature;
|
file | diff | annotate |
| 2011-04-06 |
wenzelm |
2011-04-06 |
typed_print_translation: discontinued show_sorts argument;
|
file | diff | annotate |
| 2011-04-05 |
wenzelm |
2011-04-05 |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-09-17 |
wenzelm |
2010-09-17 |
tuned signature of (Context_)Position.report variants;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-09-12 |
wenzelm |
2010-09-12 |
common Type.appl_error, which also covers explicit constraints;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-05-27 |
wenzelm |
2010-05-27 |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| 2010-05-03 |
wenzelm |
2010-05-03 |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-04-28 |
wenzelm |
2010-04-28 |
more systematic naming of tsig operations;
|
file | diff | annotate |
| 2010-04-28 |
wenzelm |
2010-04-28 |
modernized/simplified Sign.set_defsort;
|
file | diff | annotate |
| 2010-04-16 |
wenzelm |
2010-04-16 |
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
misc tuning and simplification;
|
file | diff | annotate |
| 2010-04-15 |
wenzelm |
2010-04-15 |
misc tuning and simplification;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-03-15 |
wenzelm |
2010-03-15 |
tuned;
|
file | diff | annotate |
| 2010-03-15 |
wenzelm |
2010-03-15 |
moved old Sign.intern_term to the place where it is still used;
|
file | diff | annotate |
| 2010-03-09 |
wenzelm |
2010-03-09 |
aliases for class/type/const;
tuned;
|
file | diff | annotate |
| 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.;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-03-01 |
wenzelm |
2010-03-01 |
more uniform treatment of syntax for types vs. consts;
|
file | diff | annotate |
| 2010-02-27 |
wenzelm |
2010-02-27 |
read_class: perform actual read, with source position;
|
file | diff | annotate |
| 2010-02-25 |
wenzelm |
2010-02-25 |
provide direct access to the different kinds of type declarations;
|
file | diff | annotate |
| 2010-02-21 |
wenzelm |
2010-02-21 |
slightly more abstract syntax mark/unmark operations;
|
file | diff | annotate |
| 2010-02-21 |
wenzelm |
2010-02-21 |
authentic syntax for *all* term constants;
|
file | diff | annotate |
| 2010-02-18 |
wenzelm |
2010-02-18 |
more systematic treatment of qualified names derived from binding;
|
file | diff | annotate |
| 2010-02-15 |
wenzelm |
2010-02-15 |
discontinued unnamed infix syntax;
|
file | diff | annotate |
| 2010-01-04 |
wenzelm |
2010-01-04 |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
file | diff | annotate |
| 2010-01-04 |
haftmann |
2010-01-04 |
dropped copy operation for legacy TheoryDataFun
|
file | diff | annotate |
| 2009-11-17 |
wenzelm |
2009-11-17 |
uniform new_group/reset_group;
tuned signature;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure Primitive_Defs;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
maintain theory name via name space, not tags;
AxClass.thynames_of_arity: explicit theory name, not tags;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
more direct access to naming;
tuned signature;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
maintain position of formal entities via name space;
|
file | diff | annotate |