| Sat, 13 Nov 2010 19:47:23 +0100 |
wenzelm |
eliminated slightly odd pervasive Symbol_Pos.symbol;
|
file |
diff |
annotate
|
| Sat, 30 Oct 2010 15:26:40 +0200 |
wenzelm |
support for floating-point tokens in outer syntax (coinciding with inner syntax version);
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 21:04:56 +0200 |
wenzelm |
Syntax.read_asts error: report token ranges within message -- no side-effect here;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 20:18:27 +0200 |
wenzelm |
tuned signature of (Context_)Position.report variants;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 14:08:21 +0200 |
wenzelm |
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 11:02:47 +0200 |
wenzelm |
uniform Markup.empty/Markup.Empty in ML and Scala;
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 19:54:54 +0200 |
wenzelm |
prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:00:44 +0100 |
wenzelm |
more systematic mark/unmark operations;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2009 21:55:38 +0100 |
wenzelm |
de-camelized Symbol_Pos;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 20:05:41 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 19:38:13 +0100 |
wenzelm |
added numeral, which supercedes num, xnum, float;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2008 19:27:42 +0100 |
wenzelm |
renamed terminal category "float" to "float_token", to avoid name
|
file |
diff |
annotate
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 21:26:41 +0200 |
wenzelm |
report_token/parse_token: back to context-less version;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
file |
diff |
annotate
|
| Fri, 15 Aug 2008 15:51:00 +0200 |
wenzelm |
token_kind: add Space, Comment;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 12:28:11 +0200 |
wenzelm |
pos_of_token: Position.T;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 00:09:35 +0200 |
wenzelm |
datatype token: maintain range, tuned representation;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 13:45:13 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 16:43:26 +0200 |
wenzelm |
removed obsolete read_idents;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2008 22:27:27 +0100 |
wenzelm |
basic scanners: produce symbol list instead of imploded string;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:26:28 +0200 |
wenzelm |
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
|
file |
diff |
annotate
|
| Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.tokenize: do not appen EndToken yet;
|
file |
diff |
annotate
|
| Thu, 12 Jul 2007 00:15:41 +0200 |
wenzelm |
sys_error;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:45 +0200 |
wenzelm |
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:18 +0200 |
wenzelm |
removed redundant string_of_vname (see term.ML);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:21 +0200 |
wenzelm |
avoid overloaded integer constants (accomodate Alice);
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|