| 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
|