| 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
|
| 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 09:39:27 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 18 Jan 2018 21:42:03 +0100 |
wenzelm |
unused;
|
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
|
| Sun, 07 Jan 2018 15:12:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:56:14 +0200 |
wenzelm |
tuned signature;
|
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, 31 Mar 2016 15:42:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 20:53:52 +0200 |
wenzelm |
tuned signature;
|
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, 24 Jan 2016 14:58:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 14:32:56 +0100 |
wenzelm |
tuned signature (according to Scala version);
|
file |
diff |
annotate
|
| Thu, 19 Nov 2015 22:35:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2015 22:06:14 +0100 |
wenzelm |
trim lines for @{theory_text} similarly to @{text};
|
file |
diff |
annotate
|
| Thu, 22 Oct 2015 21:16:27 +0200 |
wenzelm |
clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2015 22:25:57 +0200 |
wenzelm |
trim_blanks after read, before eval;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
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
|
| Sat, 01 Nov 2014 19:33:51 +0100 |
wenzelm |
recover via scanner;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 21:10:11 +0100 |
wenzelm |
discontinued obsolete tty and prompt;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 12:32:42 +0200 |
wenzelm |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 23:17:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 10:48:34 +0100 |
wenzelm |
clarified Token.range_of in accordance to Symbol_Pos.range;
|
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
|
| Mon, 20 Jan 2014 19:47:31 +0100 |
wenzelm |
clarified scan_cartouche_depth, according to Scala version;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 16:56:18 +0100 |
wenzelm |
tuned errors;
|
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
|
| Wed, 12 Dec 2012 17:44:10 +0100 |
wenzelm |
more systematic identifier variants to facilitate experimentation;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 15:36:51 +0100 |
wenzelm |
eliminated redundant is_ident -- more official is_identifier;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 16:07:17 +0100 |
wenzelm |
clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
|
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
|
| 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
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2012 17:46:03 +0200 |
wenzelm |
tuned messages: end-of-input rarely means physical end-of-file from the past;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 17:43:00 +0200 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 22:25:45 +0200 |
wenzelm |
proper error prefixes;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2012 14:37:43 +0200 |
wenzelm |
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
|
file |
diff |
annotate
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
file |
diff |
annotate
|
| Tue, 12 Jul 2011 14:33:08 +0200 |
wenzelm |
more precise Symbol_Pos.quote_string;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
file |
diff |
annotate
|
| Sat, 30 Apr 2011 18:16:40 +0200 |
wenzelm |
more uniform variations of scan_string;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 21:21:11 +0100 |
wenzelm |
more scalable Symbol_Pos.explode;
|
file |
diff |
annotate
|