| Sun, 14 Jan 2018 15:17:51 +0100 |
wenzelm |
clarified SML (no formal comments) vs. Isabelle/ML (arbitrary comments);
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 14:11:02 +0100 |
wenzelm |
clarified modules: uniform notion of formal comments;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 20:32:36 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 16:55:45 +0100 |
wenzelm |
allow formal comments in ML;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2017 11:32:23 +0200 |
wenzelm |
more markup for HTML rendering;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
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
|
| Thu, 22 Sep 2016 11:25:27 +0200 |
wenzelm |
discontinued raw symbols;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 15:01:43 +0200 |
wenzelm |
support rat numerals via special antiquotation syntax;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Sat, 07 Nov 2015 00:28:42 +0100 |
wenzelm |
ML cartouches via control antiquotation;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2015 20:45:33 +0200 |
wenzelm |
another antiquotation short form: undecorated cartouche as alias for @{text};
|
file |
diff |
annotate
|
| Mon, 19 Oct 2015 16:26:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 17:24:24 +0200 |
wenzelm |
support control symbol antiquotations;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2015 10:11:20 +0200 |
wenzelm |
clarified Antiquote.antiq_reports;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2014 10:44:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 15:59:30 +0100 |
wenzelm |
some special cases for official SML, to treat Isabelle symbols like raw characters;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 15:21:57 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 11:50:58 +0100 |
wenzelm |
tuned;
|
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
|
| 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 19:47:05 +0100 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 19:33:51 +0100 |
wenzelm |
recover via scanner;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 18:46:48 +0100 |
wenzelm |
simplified -- scanning is never interactive;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:09:18 +0100 |
wenzelm |
removed pointless markup;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 09:45:13 +0200 |
wenzelm |
no report for position singularity, notably for aux. file, especially empty one;
|
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
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 20:53:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 16:34:02 +0100 |
wenzelm |
generic markup for embedded languages;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 18:28:18 +0100 |
wenzelm |
more uniform ML keyword markup;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 20:58:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:04:52 +0100 |
wenzelm |
tuned -- more direct err_prefix;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 16:56:18 +0100 |
wenzelm |
tuned errors;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 15:36:54 +0200 |
wenzelm |
discontinued unused antiquotation blocks;
|
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
|
| Sat, 11 Aug 2012 17:24:21 +0200 |
wenzelm |
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 15:57:22 +0200 |
wenzelm |
sneak message into "bad" markup as property -- to be displayed after YXML parsing;
|
file |
diff |
annotate
|
| Fri, 10 Aug 2012 10:18:07 +0200 |
wenzelm |
more visible markup of malformed input as "bad";
|
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
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 19:36:19 +0200 |
wenzelm |
eliminated markup for plain identifiers (frequent but insignificant);
|
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
|
| Mon, 10 Jan 2011 21:45:44 +0100 |
wenzelm |
refined ML_Lex.flatten: ensure proper separation of tokens;
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:47:23 +0100 |
wenzelm |
eliminated slightly odd pervasive Symbol_Pos.symbol;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:21:53 +0100 |
wenzelm |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 10:33:37 +0100 |
wenzelm |
warn in correlation with report -- avoid spurious message duplicates;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 13:54:23 +0100 |
wenzelm |
explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 18:17:48 +0200 |
wenzelm |
terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|