| Sun, 05 Dec 2021 15:54:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 24 Nov 2021 15:33:43 +0100 |
wenzelm |
more uniform treatment of optional_argument for Latex elements;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 20:46:40 +0100 |
wenzelm |
more general document output: enclosing markup is defined in user-space;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 12:29:09 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 12:04:01 +0100 |
wenzelm |
tuned signature: more explicit types for presentation;
|
file |
diff |
annotate
|
| Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 20 May 2021 13:50:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 May 2021 21:42:45 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 17:24:24 +0100 |
wenzelm |
more markup for various text kinds, notably for nested formal comments;
|
file |
diff |
annotate
|
| Sat, 03 Feb 2018 14:39:17 +0100 |
wenzelm |
avoid proliferation of language_document reports;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 23:45:43 +0100 |
wenzelm |
theory Pure is default presentation context;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 22:09:23 +0200 |
wenzelm |
section headings for ROOT.ML;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2016 17:37:20 +0100 |
wenzelm |
discontinued old 'header';
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 21:26:14 +0200 |
wenzelm |
more uniform command setup;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 21:15:10 +0200 |
wenzelm |
added 'paragraph', 'subparagraph';
|
file |
diff |
annotate
|
| Fri, 16 Oct 2015 10:11:20 +0200 |
wenzelm |
clarified Antiquote.antiq_reports;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2015 11:09:26 +0200 |
wenzelm |
clarified language context, e.g. relevant for symbols;
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 19:48:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:11:04 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:00:03 +0200 |
wenzelm |
more explicit bootstrap_thy;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
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
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:35:11 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:59:15 +0200 |
wenzelm |
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 17:23:05 +0200 |
wenzelm |
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:56:13 +0100 |
wenzelm |
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
|
file |
diff |
annotate
|