| 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
|
| Mon, 27 May 2013 22:25:32 +0200 |
wenzelm |
more literal tokens, e.g. "EX!";
|
file |
diff |
annotate
|
| Thu, 04 Apr 2013 12:06:23 +0200 |
wenzelm |
added var_position in analogy to longid_position, for typing reports on input;
|
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
|
| Mon, 26 Nov 2012 21:10:42 +0100 |
wenzelm |
more uniform Symbol.is_ascii_identifier in ML/Scala;
|
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
|
| Thu, 11 Oct 2012 20:38:02 +0200 |
wenzelm |
clarified output token markup (see also bc22daeed49e);
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 12:25:27 +0100 |
wenzelm |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
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
|
| Sat, 18 Jun 2011 12:37:42 +0200 |
wenzelm |
inner literal/delimiter corresponds to outer keyword/operator;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 21:05:52 +0200 |
wenzelm |
clarified auxiliary structure Lexicon.Syntax;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 23:04:00 +0200 |
wenzelm |
separate structure Term_Position;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 16:15:50 +0100 |
wenzelm |
update_name_tr: more precise handling of explicit constraints, including positions;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
file |
diff |
annotate
|
| Mon, 21 Mar 2011 23:38:32 +0100 |
wenzelm |
added Lexicon.encode_position, Lexicon.decode_position;
|
file |
diff |
annotate
|
| 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
|
| Tue, 12 Dec 2006 00:25:09 +0100 |
wenzelm |
read_xnum: return leading_zeros, radix;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 21:41:03 +0100 |
wenzelm |
xstr: disallow backslashes;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:07 +0200 |
wenzelm |
renamed Syntax.indexname to Syntax.read_indexname;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:12:08 +0200 |
wenzelm |
export is_tid;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 14:21:08 +0200 |
wenzelm |
uniform treatment of num/xnum;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:22:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 00:43:54 +0200 |
kleing |
hex and binary numerals (contributed by Rafal Kolanski)
|
file |
diff |
annotate
|