| Sun, 24 Sep 2023 15:55:42 +0200 |
wenzelm |
clarified signature;
|
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
|
| Sat, 20 May 2023 22:41:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:18:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 16:12:37 +0200 |
wenzelm |
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
|
file |
diff |
annotate
|
| Thu, 18 May 2023 23:50:59 +0200 |
wenzelm |
more careful reset/set_context for stored declarations;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
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
|
| Fri, 14 Apr 2023 20:42:17 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Sat, 01 Apr 2023 14:50:43 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
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
|
| Thu, 21 Oct 2021 18:10:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 20:04:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:36:49 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 16:01:13 +0200 |
wenzelm |
outer syntax: support for control-cartouche tokens;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2021 20:18:00 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2021 14:24:57 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2021 12:54:28 +0200 |
wenzelm |
clarified signature;
|
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
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Fri, 01 Mar 2019 16:49:41 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:21:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:11:24 +0200 |
wenzelm |
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
|
file |
diff |
annotate
|
| Sun, 27 May 2018 13:42:01 +0200 |
wenzelm |
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
|
file |
diff |
annotate
|
| Mon, 14 May 2018 22:01:00 +0200 |
wenzelm |
adjust position according to offset of command/exec id;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Jan 2018 11:29:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Jan 2018 11:20:31 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 20:47:36 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 20:08:33 +0100 |
wenzelm |
tuned signature: removed unused operations;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 16:34:24 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 11:56:38 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 11:27:52 +0100 |
wenzelm |
discontinued old form of marginal comments;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 23:03:01 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 22:46:04 +0100 |
wenzelm |
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2017 11:32:23 +0200 |
wenzelm |
more markup for HTML rendering;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2017 10:58:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 08 Jun 2017 23:04:07 +0200 |
wenzelm |
more HTML rendering as in Isabelle/jEdit;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 17:08:21 +0100 |
wenzelm |
avoid extra decorations for regular command keywords;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
file |
diff |
annotate
|
| Thu, 27 Oct 2016 21:52:12 +0200 |
wenzelm |
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2016 11:25:27 +0200 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2016 19:44:28 +0200 |
wenzelm |
print name in parsable form;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:56:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:49:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 16:23:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 16:10:13 +0100 |
wenzelm |
prefer non-ASCII output;
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 15:53:28 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 21:20:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 21:10:45 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 20:58:09 +0100 |
wenzelm |
tuned;
|
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
|
| Tue, 10 Nov 2015 19:03:29 +0100 |
wenzelm |
added document antiquotation @{theory_text};
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 17:24:24 +0200 |
wenzelm |
support control symbol antiquotations;
|
file |
diff |
annotate
|