| Fri, 14 Apr 2023 20:42:17 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Wed, 27 Jan 2021 14:56:40 +0100 |
wenzelm |
tuned signature (e.g. see HTML.control_block in Isabelle/Scala);
|
file |
diff |
annotate
|
| Tue, 19 Jan 2021 20:23:13 +0100 |
wenzelm |
suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff);
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
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
|
| Sun, 25 Nov 2018 18:45:10 +0100 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2018 14:33:30 +0100 |
wenzelm |
more comment markup;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 19:59:53 +0200 |
wenzelm |
discontinued old-style inner comments;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:11:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:02:37 +0100 |
wenzelm |
more efficient tokens_match_ord based on token_kind_index;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:49:56 +0100 |
wenzelm |
more abstract type;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:40:26 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:26:50 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:23:53 +0100 |
wenzelm |
explicit dummy token;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:18:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:09:05 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 18:38:18 +0100 |
wenzelm |
tuned data structure and operations;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 11:48:38 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 23:03:01 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 15:06:27 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 14:11:02 +0100 |
wenzelm |
clarified modules: uniform notion of formal comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 11:22:46 +0100 |
wenzelm |
added \<^cancel> operator for unused text;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 20:19:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 17:09:34 +0100 |
wenzelm |
clarified markup: more like outer syntax side-comment;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 21:28:03 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 15:12:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 06 Jan 2018 16:56:07 +0100 |
wenzelm |
inner syntax comments may be written as "\<comment> \<open>text\<close>";
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:46:51 +0200 |
wenzelm |
accomodate Poly/ML repository version, which treats singleton strings as boxed;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 16:23:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 20:53:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 21:28:57 +0200 |
wenzelm |
discontinued old "xnum" token category;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 21:32:09 +0100 |
wenzelm |
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 17:51:16 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:10:33 +0100 |
wenzelm |
inner syntax token language allows regular quoted strings;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:38:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:24:44 +0100 |
wenzelm |
tuned error messages, more accurate position;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:04:52 +0100 |
wenzelm |
tuned -- more direct err_prefix;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:31:32 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 22:56:28 +0100 |
wenzelm |
discontinued legacy_isub_isup;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:26:22 +0200 |
wenzelm |
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 17:36:14 +0200 |
wenzelm |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 16:25:26 +0200 |
wenzelm |
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
|
file |
diff |
annotate
|
| Mon, 27 May 2013 22:25:32 +0200 |
wenzelm |
more literal tokens, e.g. "EX!";
|
file |
diff |
annotate
|
| Thu, 04 Apr 2013 12:06:23 +0200 |
wenzelm |
added var_position in analogy to longid_position, for typing reports on input;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 19:22:36 +0100 |
wenzelm |
support for sub-structured identifier syntax (inactive);
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:10:42 +0100 |
wenzelm |
more uniform Symbol.is_ascii_identifier in ML/Scala;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 20:38:02 +0200 |
wenzelm |
clarified output token markup (see also bc22daeed49e);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|