| Tue, 29 Aug 2023 17:00:12 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 15:48:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 15:45:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 15:42:13 +0100 |
wenzelm |
tunes signature;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 16:19:59 +0200 |
wenzelm |
clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 18:35:59 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 12:18:06 +0200 |
wenzelm |
clarified theory_names with exported content;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 12:01:47 +0200 |
wenzelm |
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
|
file |
diff |
annotate
|
| Sun, 07 Aug 2022 12:58:59 +0200 |
wenzelm |
clarified signature: more uniform treatment of cache for Export.read_session vs. Export.read_theory;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2022 22:49:25 +0200 |
wenzelm |
discontinued Export.Provider in favour of Export.Context and its derivatives;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2022 19:02:38 +0200 |
wenzelm |
clarified database query: refer to semantic theories;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2022 14:05:42 +0200 |
wenzelm |
more uniform exports: proper encoding of empty parents for Pure;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2022 13:44:21 +0200 |
wenzelm |
clarified signature: Export.Provider knows its (accidental) theory_names;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2022 13:07:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2022 12:58:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2022 11:23:12 +0200 |
wenzelm |
removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);
|
file |
diff |
annotate
|
| Sat, 30 Jul 2022 11:35:04 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2022 15:28:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2022 12:02:38 +0200 |
wenzelm |
avoid pattern-match warnings, notably in scala3;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2021 15:03:37 +0100 |
wenzelm |
more compact data during presentation: Entity_Context.Theory_Export instead of full Export_Theory.Theory;
|
file |
diff |
annotate
|
| Fri, 05 Nov 2021 20:42:06 +0100 |
wenzelm |
more compact persistent data;
|
file |
diff |
annotate
|
| Thu, 04 Nov 2021 19:22:11 +0100 |
wenzelm |
clarified Theory_Cache: prefer immutable data with Synchronized variable;
|
file |
diff |
annotate
|
| Thu, 04 Nov 2021 15:44:37 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 04 Nov 2021 12:01:28 +0100 |
wenzelm |
tuned -- eliminate clones stemming from d28a51dd9da6;
|
file |
diff |
annotate
|
| Tue, 02 Nov 2021 15:40:02 +0100 |
wenzelm |
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;
|
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, 04 Aug 2021 21:03:25 +0200 |
wenzelm |
more operations: record overall exported entities;
|
file |
diff |
annotate
|
| Wed, 04 Aug 2021 19:41:59 +0200 |
wenzelm |
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
|
file |
diff |
annotate
|
| Fri, 18 Jun 2021 15:03:12 +0200 |
wenzelm |
tuned --- following hints by IntelliJ;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 22:22:34 +0100 |
wenzelm |
clarified signature: absorb XZ.Cache into XML.Cache;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 15:58:48 +0100 |
wenzelm |
clarified signature --- internal Cache.none;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 20:26:09 +0100 |
wenzelm |
clarified signature: provide XZ.Cache where Export.Entry is created;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 15:24:55 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 23 Nov 2020 13:52:14 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 07 Apr 2020 21:49:36 +0200 |
wenzelm |
clarified signature: more uniform treatment of stopped/interrupted state;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 16:13:36 +0100 |
wenzelm |
discontinued somewhat pointless options;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 15:44:55 +0100 |
wenzelm |
export datatypes;
|
file |
diff |
annotate
|
| Tue, 03 Dec 2019 16:40:04 +0100 |
wenzelm |
clarified export of consts: recursion is accessible via spec_rules;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 13:03:09 +0100 |
wenzelm |
more informative export;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 11:57:42 +0100 |
wenzelm |
clarified export of spec rules: more like locale;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2019 21:29:08 +0100 |
wenzelm |
formal position for spec rule (not significant for equality);
|
file |
diff |
annotate
|
| Sat, 30 Nov 2019 15:17:23 +0100 |
wenzelm |
export spec rules;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 19:43:59 +0100 |
wenzelm |
clarified errors;
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 18:55:35 +0100 |
wenzelm |
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
|
file |
diff |
annotate
|
| Mon, 21 Oct 2019 16:32:10 +0200 |
wenzelm |
export constdefs according to defs.ML;
|
file |
diff |
annotate
|
| Sun, 20 Oct 2019 12:56:36 +0200 |
wenzelm |
more kinds, notably for Isabelle/MMT;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2019 16:25:54 +0200 |
wenzelm |
clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 21:03:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 16:10:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 17 Oct 2019 14:06:14 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 21:05:35 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:41:47 +0200 |
wenzelm |
more support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 16:04:11 +0200 |
wenzelm |
support for proof terms;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2019 14:14:10 +0200 |
wenzelm |
clarified proof export;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 13:43:17 +0200 |
wenzelm |
more compact XML: separate environment for free variables;
|
file |
diff |
annotate
|