src/Pure/sign.ML
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Sat, 04 Apr 2015 14:04:11 +0200 wenzelm support private scope for individual local theory commands;
Wed, 01 Apr 2015 18:17:44 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 22:31:05 +0200 wenzelm support for explicit scope of private entries;
Tue, 31 Mar 2015 17:34:52 +0200 wenzelm clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Fri, 21 Mar 2014 11:06:39 +0100 wenzelm tuned signature;
Fri, 21 Mar 2014 10:45:03 +0100 wenzelm tuned signature;
Wed, 12 Mar 2014 10:42:28 +0100 wenzelm more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
Tue, 11 Mar 2014 22:49:28 +0100 wenzelm 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;
Mon, 10 Mar 2014 15:04:01 +0100 wenzelm tuned signature -- prefer Name_Space.get with its builtin error;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
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;
less more (0) -300 -100 -60 tip