| Thu, 19 Sep 2024 12:41:02 +0200 |
wenzelm |
minor performance tuning: avoid vacuous update of context;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 11:09:35 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 15:55:36 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 12:34:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 11:22:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 22:10:16 +0100 |
wenzelm |
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 11:06:36 +0200 |
wenzelm |
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 20:09:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 19:41:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Sun, 12 May 2013 18:22:44 +0200 |
wenzelm |
support for system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 21:47:47 +0200 |
wenzelm |
avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;
|
file |
diff |
annotate
|
| Sat, 30 Oct 2010 16:33:58 +0200 |
wenzelm |
support for real valued configuration options;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 21:33:19 +0200 |
wenzelm |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:09:12 +0200 |
wenzelm |
more explicit Config.declare vs. Config.declare_global;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 17:02:19 +0200 |
wenzelm |
tuned printed type names, according to ML;
|
file |
diff |
annotate
|
| Mon, 10 May 2010 20:53:06 +0200 |
wenzelm |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 17:43:09 +0200 |
wenzelm |
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:13:29 +0200 |
wenzelm |
configuration options admit dynamic default values;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 12:06:28 +0200 |
wenzelm |
added name_of;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:42 +0200 |
wenzelm |
renamed config_option.ML to config.ML;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 20:11:47 +0200 |
wenzelm |
map_value: dynamic type checking;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 16:31:14 +0200 |
wenzelm |
exported datatype value;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 22:20:49 +0200 |
wenzelm |
Configuration options as values within the local context.
|
file |
diff |
annotate
|