| Tue, 20 Feb 2018 14:03:31 +0100 |
wenzelm |
use lazy notes for locale context init and later additions of facts;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 22:07:21 +0100 |
wenzelm |
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:24:17 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 15:46:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:49:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 20:08:21 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:49:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:41:25 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 12:54:31 +0200 |
wenzelm |
eliminated suspicious Unicode;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 11:33:32 +0200 |
ballarin |
Update header of locale.ML
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
prefer explicit datatype over implicit sum;
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 17:44:26 +0200 |
ballarin |
Improved error reporting when activating a locale instance (beyond syntax decls).
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 20:08:40 +0200 |
ballarin |
Improved error reporting when activating a locale instance.
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:02:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 11:40:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2016 11:14:10 +0200 |
wenzelm |
avoid massive multiplication of reports due to interpretation;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 15:53:12 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 21:10:45 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Sat, 21 Nov 2015 23:02:07 +0100 |
ballarin |
Clarify locale qualifiers: output and tutorial.
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 21:54:32 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 19:47:37 +0200 |
wenzelm |
more thorough transfer;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 15:49:12 +0200 |
wenzelm |
clarified vacuous binding;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 13:26:29 +0200 |
wenzelm |
trim context more thoroughly;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 11:36:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 05:12:14 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 18:39:32 +0100 |
haftmann |
formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:30:28 +0200 |
wenzelm |
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 16:21:27 +0200 |
wenzelm |
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:29:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 12:23:59 +0100 |
wenzelm |
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 20:42:08 +0100 |
wenzelm |
reverted c05d3e22adaf: Locale.intern is still required by AFP/Simpl;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 21:30:35 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 13:45:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 20:21:22 +0100 |
haftmann |
initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 20:37:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 14:13:18 +0200 |
wenzelm |
recovered Locale.intern from d51bac27d4a0 (still used in AFP/Simp);
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 20:58:15 +0200 |
wenzelm |
more markup -- avoid old Locale.extern;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:40:56 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 21 May 2013 17:45:53 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
tuned for uniformity
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 22:36:03 +0100 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 19:53:44 +0100 |
ballarin |
Fix issue related to mixins in roundup.
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|