| Sat, 02 Dec 2023 15:42:50 +0100 |
wenzelm |
pro-forma support for optional zproof: no proper content yet;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 10:56:45 +0200 |
wenzelm |
distinguish proper interrupts from Poly/ML RTS breakdown;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2023 11:27:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 14:43:07 +0200 |
wenzelm |
clarified treatment of exceptions: avoid catch-all handlers;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2023 12:35:14 +0200 |
wenzelm |
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2023 20:15:31 +0200 |
wenzelm |
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
|
file |
diff |
annotate
|
| Wed, 10 May 2023 20:30:46 +0200 |
wenzelm |
more informative position information;
|
file |
diff |
annotate
|
| Sat, 22 Apr 2023 21:00:24 +0200 |
wenzelm |
tuned: concise combinators instead of bulky case-expressions;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 16:17:29 +0100 |
wenzelm |
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 15:54:49 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 15:39:18 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 14:54:32 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 13:00:16 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 12:34:40 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 12:27:55 +0100 |
wenzelm |
discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 12:08:58 +0100 |
wenzelm |
tuned --- more robust ML patterns;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2022 11:49:11 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 20:10:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 14:50:43 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2022 12:44:02 +0200 |
wenzelm |
option "show_states" for more verbosity of batch-builds;
|
file |
diff |
annotate
|
| Tue, 15 Feb 2022 16:16:53 +0100 |
wenzelm |
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2021 22:11:10 +0100 |
wenzelm |
allow general command transactions with presentation;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 16:06:09 +0100 |
wenzelm |
output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 12:04:01 +0100 |
wenzelm |
tuned signature: more explicit types for presentation;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2021 16:19:49 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Oct 2021 10:58:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2021 15:44:10 +0200 |
wenzelm |
maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche;
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
|
| Wed, 12 May 2021 16:47:52 +0200 |
wenzelm |
clarified signature: provide access to previous state;
|
file |
diff |
annotate
|
| Sun, 02 May 2021 15:22:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 16:59:27 +0100 |
wenzelm |
discontinued body_range (again): does not quite work, because Position.thread_data is plain Toplevel.pos_of only;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 14:40:04 +0100 |
wenzelm |
support more command positions, analogous to Command.core_range in Isabelle/Scala;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2020 15:16:54 +0000 |
haftmann |
tuned interfaces
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
dedicated module for toplevel target handling
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
centralized case distinction for beginning and ending nested targets in one place
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:51:40 +0000 |
haftmann |
direct exit to theory when ending nested target on theory target
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:43:09 +0000 |
haftmann |
consolidated terminology
|
file |
diff |
annotate
|
| Mon, 04 Nov 2019 20:10:23 +0100 |
wenzelm |
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
|
file |
diff |
annotate
|
| Tue, 23 Jul 2019 12:07:50 +0200 |
wenzelm |
proof terms are always constructed sequentially;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 17:09:21 +0200 |
wenzelm |
support "tag" marker with scope;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:23:52 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 10:31:20 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 21:18:58 +0100 |
wenzelm |
tuned -- more explicit type node_presentation;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 19:22:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 19:36:17 +0100 |
wenzelm |
Backed out changeset 1bc422c08209 -- obsolete in AFP/5d11846ac6ab;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 15:29:22 +0100 |
wenzelm |
keep Local_Theory.reset for now -- still required in many AFP sessions (amending 1c201e4792cb);
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 07:08:27 +0000 |
haftmann |
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 19:48:15 +0200 |
wenzelm |
clarified reset_notepad;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 14:56:26 +0200 |
wenzelm |
more robust reset_state: begin/end structure takes precedence over goal/proof structure;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 14:14:43 +0200 |
wenzelm |
no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 13:53:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 17:16:36 +0200 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2018 11:44:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 11:26:31 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:01:46 +0200 |
wenzelm |
clarified default tag;
|
file |
diff |
annotate
|