| Tue, 30 Jan 2018 11:48:38 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 23:03:01 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 15:06:27 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 14:11:02 +0100 |
wenzelm |
clarified modules: uniform notion of formal comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 11:22:46 +0100 |
wenzelm |
added \<^cancel> operator for unused text;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 20:19:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 17:09:34 +0100 |
wenzelm |
clarified markup: more like outer syntax side-comment;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 21:28:03 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 15:12:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 06 Jan 2018 16:56:07 +0100 |
wenzelm |
inner syntax comments may be written as "\<comment> \<open>text\<close>";
|
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
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 16:23:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 20:53:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 21:28:57 +0200 |
wenzelm |
discontinued old "xnum" token category;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 21:32:09 +0100 |
wenzelm |
special identifier "__" (i.e. empty name with internal suffix) serves as wild-card for completion;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 17:51:16 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:10:33 +0100 |
wenzelm |
inner syntax token language allows regular quoted strings;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:38:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:24:44 +0100 |
wenzelm |
tuned error messages, more accurate position;
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:04:52 +0100 |
wenzelm |
tuned -- more direct err_prefix;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:31:32 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 22:56:28 +0100 |
wenzelm |
discontinued legacy_isub_isup;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:26:22 +0200 |
wenzelm |
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 17:36:14 +0200 |
wenzelm |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
file |
diff |
annotate
|
| 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
|