| Wed, 28 Feb 2024 17:25:54 +0100 |
Fabian Huch |
add option for unify trace (now disabled by default as printing is excessive and rarely used);
|
file |
diff |
annotate
|
| Wed, 28 Feb 2024 15:19:15 +0100 |
Fabian Huch |
tuned unify trace option names;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 15:00:48 +0100 |
wenzelm |
clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
|
file |
diff |
annotate
|
| Sun, 24 Dec 2023 12:06:20 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 24 Dec 2023 11:58:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 20:07:30 +0200 |
wenzelm |
explicitly reject 'handle' with catch-all patterns;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 20:11:15 +0200 |
wenzelm |
clarified output of embedded values, e.g. for 'print_locale';
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 22:49:20 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 21:23:44 +0200 |
wenzelm |
tuned --- Token.make_string / Token.assign are value-oriented;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:18:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 14:06:35 +0200 |
wenzelm |
proper Token.Declaration for internal_declaration;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 17:08:31 +0200 |
wenzelm |
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
|
file |
diff |
annotate
|
| Wed, 10 May 2023 21:17:21 +0200 |
wenzelm |
more informative position information;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 21:18:40 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 21:13:29 +0200 |
wenzelm |
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2021 23:04:58 +0200 |
wenzelm |
support configuration options "show_results";
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 10:33:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 13:28:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 21:29:08 +0200 |
wenzelm |
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 20:43:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 14:42:24 +0200 |
wenzelm |
support named ML environments, notably "Isabelle", "SML";
|
file |
diff |
annotate
|
| Sun, 01 Jul 2018 12:38:37 +0200 |
wenzelm |
discontinued pending_shyps: too much complication due to lazy facts;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 15:54:41 +0200 |
wenzelm |
disallow pending hyps;
|
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
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 18:25:35 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 11:03:24 +0200 |
wenzelm |
tuned;
|
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
|
| Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 15:42:52 +0200 |
wenzelm |
unfold is subject to unfold_abs_def (still inactive);
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 12:13:11 +0200 |
wenzelm |
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:51:37 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:14:27 +0200 |
wenzelm |
removed redundant Position.set_range -- already done in Position.range;
|
file |
diff |
annotate
|
| Wed, 02 Mar 2016 19:43:31 +0100 |
wenzelm |
support for ML_exception_debugger;
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 16:01:57 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 20:58:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 18:45:46 +0100 |
wenzelm |
unused;
|
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
|
| Fri, 30 Oct 2015 17:14:30 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 16:03:11 +0200 |
wenzelm |
proper attribute;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:36:46 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 17:19:27 +0200 |
wenzelm |
tuned output -- avoid empty quites and extra breaks;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 19:47:48 +0100 |
wenzelm |
tuned signature (see ab2483fad861);
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 12:32:42 +0200 |
wenzelm |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 12:58:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 10:07:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 14:28:11 +0200 |
wenzelm |
localized command 'method_setup' and 'attribute_setup';
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:33:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 11:55:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:57:55 +0200 |
wenzelm |
localized attribute definitions;
|
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
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 19:03:02 +0100 |
wenzelm |
proper configuration option "ML_print_depth";
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:54:38 +0100 |
wenzelm |
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 12:00:17 +0100 |
wenzelm |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
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 20:27:08 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 18:06:23 +0100 |
wenzelm |
clarified Args.check_src: retain name space information for error output;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 16:30:07 +0100 |
wenzelm |
clarified Args.src: more abstract type, position refers to name only;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:20:41 +0100 |
wenzelm |
prefer Name_Space.pretty with its builtin markup;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:04:01 +0100 |
wenzelm |
tuned signature -- prefer Name_Space.get with its builtin error;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:31:12 +0100 |
wenzelm |
keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 11:36:04 +0100 |
wenzelm |
more positions;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 18:18:03 +0100 |
wenzelm |
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 22:39:31 +0200 |
wenzelm |
more markup via Name_Space.check;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2013 17:35:12 +0200 |
wenzelm |
turned pattern unify flag into configuration option (global only);
|
file |
diff |
annotate
|
| Wed, 17 Jul 2013 11:38:57 +0200 |
wenzelm |
more official Thm.eq_thm_strict, without demanding ML equality type;
|
file |
diff |
annotate
|
| Sun, 30 Jun 2013 11:37:34 +0200 |
wenzelm |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 23:17:26 +0200 |
wenzelm |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:53:28 +0200 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 20:33:01 +0200 |
wenzelm |
system options as context-sensitive configuration options within the attribute name space;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 19:41:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2013 11:38:16 +0100 |
webertj |
Typo in description of abs_def.
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 16:23:07 +0100 |
wenzelm |
allow negative argument in "consumes" source format;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 16:17:46 +0200 |
wenzelm |
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 06 Jul 2012 16:20:54 +0200 |
wenzelm |
discontinued obsolete attribute "COMP";
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:58:29 +0200 |
wenzelm |
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|