src/Pure/sign.ML
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Sun, 18 Mar 2012 13:59:54 +0100 wenzelm comment;
Sun, 18 Mar 2012 13:37:11 +0100 wenzelm tuned;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Fri, 25 Nov 2011 16:32:29 +0100 wenzelm prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
Wed, 09 Nov 2011 17:57:42 +0100 wenzelm sort assignment before simultaneous term_check, not isolated parse_term;
Wed, 13 Jul 2011 20:36:18 +0200 wenzelm sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Mon, 18 Apr 2011 13:52:23 +0200 wenzelm standardized aliases of operations on tsig;
Mon, 18 Apr 2011 13:26:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 20:15:46 +0200 wenzelm eliminated obsolete markup -- superseded by generic "entity" markup;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 15:25:25 +0200 wenzelm prefer local name spaces;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Fri, 08 Apr 2011 18:08:13 +0200 wenzelm simplified Pure syntax bootstrap;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 08 Apr 2011 15:02:11 +0200 wenzelm discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Thu, 07 Apr 2011 18:24:59 +0200 wenzelm discontinued user-defined token translations;
Wed, 06 Apr 2011 13:33:46 +0200 wenzelm typed_print_translation: discontinued show_sorts argument;
Tue, 05 Apr 2011 14:25:18 +0200 wenzelm discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
Sun, 03 Apr 2011 21:59:33 +0200 wenzelm added Position.reports convenience;
Sat, 04 Dec 2010 18:41:12 +0100 wenzelm added Syntax.default_root;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Sun, 12 Sep 2010 19:55:45 +0200 wenzelm common Type.appl_error, which also covers explicit constraints;
Sun, 05 Sep 2010 23:16:21 +0200 wenzelm turned show_brackets into proper configuration option;
Sun, 05 Sep 2010 19:47:40 +0200 wenzelm pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Wed, 28 Apr 2010 11:13:11 +0200 wenzelm more systematic naming of tsig operations;
Wed, 28 Apr 2010 11:09:19 +0200 wenzelm modernized/simplified Sign.set_defsort;
Fri, 16 Apr 2010 22:45:07 +0200 wenzelm replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
Thu, 15 Apr 2010 20:37:27 +0200 wenzelm misc tuning and simplification;
Sat, 27 Mar 2010 17:36:32 +0100 wenzelm disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Mon, 15 Mar 2010 21:59:28 +0100 wenzelm tuned;
Mon, 15 Mar 2010 21:57:35 +0100 wenzelm moved old Sign.intern_term to the place where it is still used;
Tue, 09 Mar 2010 23:29:04 +0100 wenzelm aliases for class/type/const;
Tue, 09 Mar 2010 14:35:02 +0100 wenzelm added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
Wed, 03 Mar 2010 00:28:22 +0100 wenzelm authentic syntax for classes and type constructors;
Mon, 01 Mar 2010 17:07:36 +0100 wenzelm more uniform treatment of syntax for types vs. consts;
Sat, 27 Feb 2010 13:32:18 +0100 wenzelm read_class: perform actual read, with source position;
Thu, 25 Feb 2010 22:05:34 +0100 wenzelm provide direct access to the different kinds of type declarations;
Sun, 21 Feb 2010 22:35:02 +0100 wenzelm slightly more abstract syntax mark/unmark operations;
Sun, 21 Feb 2010 21:08:25 +0100 wenzelm authentic syntax for *all* term constants;
Thu, 18 Feb 2010 20:46:46 +0100 wenzelm more systematic treatment of qualified names derived from binding;
Mon, 15 Feb 2010 17:17:51 +0100 wenzelm discontinued unnamed infix syntax;
Mon, 04 Jan 2010 23:20:35 +0100 wenzelm 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);
Mon, 04 Jan 2010 14:09:56 +0100 haftmann dropped copy operation for legacy TheoryDataFun
Tue, 17 Nov 2009 14:50:55 +0100 wenzelm uniform new_group/reset_group;
Mon, 02 Nov 2009 20:38:46 +0100 wenzelm modernized structure Primitive_Defs;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sun, 25 Oct 2009 20:54:21 +0100 wenzelm maintain theory name via name space, not tags;
Sun, 25 Oct 2009 19:17:42 +0100 wenzelm more direct access to naming;
Sun, 25 Oct 2009 12:27:21 +0100 wenzelm allow name space entries to be "concealed" -- via binding/naming/local_theory;
less more (0) -300 -100 -60 tip