| Sun, 04 Mar 2012 16:02:14 +0100 |
wenzelm |
clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 20:29:39 +0200 |
wenzelm |
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
|
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
|
| Tue, 12 Jul 2011 14:33:08 +0200 |
wenzelm |
more precise Symbol_Pos.quote_string;
|
file |
diff |
annotate
|
| Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
file |
diff |
annotate
|
| Sat, 30 Apr 2011 18:16:40 +0200 |
wenzelm |
more uniform variations of scan_string;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 15:14:28 +0100 |
wenzelm |
eliminated obsolete Token.Malformed -- subsumed by Token.Error;
|
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 21:01:03 +0100 |
wenzelm |
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
|
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
|
| 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
|
| Sat, 07 Aug 2010 21:22:39 +0200 |
wenzelm |
more robust treatment of Markup.token;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2010 21:03:06 +0200 |
wenzelm |
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
| base
|