| 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
|
| Sun, 30 May 2010 16:00:13 +0200 |
wenzelm |
separate markup for ML delimiters;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 11:12:40 +0200 |
wenzelm |
allow Isabelle symbols within low-level ML source;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 19:58:11 +0200 |
wenzelm |
export end_pos_of;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 17:31:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 23:28:05 +0200 |
wenzelm |
added flatten;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 11:57:41 +0100 |
wenzelm |
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:50:02 +0100 |
wenzelm |
added read_antiq, with improved error reporting;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 19:10:59 +0100 |
wenzelm |
ML_Lex.pos_of: regular position;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 20:22:13 +0100 |
wenzelm |
report markup for ML tokens;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 09:51:41 +0100 |
wenzelm |
allow non-printable symbols within string tokens;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 21:04:53 +0100 |
wenzelm |
added scan_antiq;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 18:20:27 +0100 |
wenzelm |
added tokenize;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:59 +0200 |
wenzelm |
renamed ML_Lex.val_of to content_of;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 00:09:34 +0200 |
wenzelm |
tuned SymbolPos interface;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 13:45:11 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 21:24:17 +0200 |
wenzelm |
abstract type Scan.stopper;
|
file |
diff |
annotate
|
| Sun, 16 Sep 2007 14:52:31 +0200 |
wenzelm |
removed obsolete Selector token;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:25:43 +0200 |
wenzelm |
Lexical syntax for SML.
|
file |
diff |
annotate
|