| Tue, 23 Nov 2021 21:43:45 +0100 |
wenzelm |
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2021 17:14:55 +0100 |
wenzelm |
clarified modules (see c299abcf7081);
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 13:44:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 00:16:23 +0100 |
wenzelm |
updated to 146757999c8d;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 11:38:19 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 21:27:17 +0200 |
wenzelm |
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 19:48:54 +0200 |
wenzelm |
clarified conditional compilation;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Sat, 26 Dec 2015 15:59:27 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2015 10:11:20 +0200 |
wenzelm |
clarified Antiquote.antiq_reports;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 19:48:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 11:39:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
| Thu, 11 Dec 2014 15:24:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2014 19:26:01 +0100 |
wenzelm |
more examples;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 20:45:11 +0100 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 14:43:00 +0100 |
wenzelm |
update_cartouches;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 14:02:48 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
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
|
| 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 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
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 20:58:32 +0200 |
wenzelm |
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 17:54:09 +0200 |
wenzelm |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
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
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 22:57:50 +0100 |
wenzelm |
tuned signature -- clarified module name;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 13:55:09 +0100 |
wenzelm |
simplified inner syntax;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:28:19 +0100 |
wenzelm |
avoid breakdown of document preparation, which does not understand cartouche tokens yet;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:11:10 +0100 |
wenzelm |
more cartouche examples, including uniform nesting of sub-languages;
|
file |
diff |
annotate
|
| Sun, 19 Jan 2014 21:33:45 +0100 |
wenzelm |
implicit "cartouche" method (experimental, undocumented);
|
file |
diff |
annotate
|
| Sun, 19 Jan 2014 21:00:42 +0100 |
wenzelm |
more examples;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:35:42 +0100 |
wenzelm |
proper \<newline>;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|