| Wed, 26 Sep 2018 17:04:50 +0200 |
wenzelm |
clarified get_infix: avoid old ASCII input syntax;
|
file |
diff |
annotate
|
| Sun, 16 Sep 2018 22:45:34 +0200 |
wenzelm |
export plain infix syntax;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 22:43:06 +0200 |
wenzelm |
more general mixfix delimiters;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 22:20:03 +0200 |
wenzelm |
explicit warning about formal use of Unicode;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 21:34:17 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 19:01:34 +0200 |
wenzelm |
require actual space;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 18:43:54 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 18:32:52 +0200 |
wenzelm |
clarified errors -- disallow cartouche fragments as delimiter;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:14:27 +0200 |
wenzelm |
removed redundant Position.set_range -- already done in Position.range;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 15:27:59 +0200 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 14:49:02 +0200 |
wenzelm |
clarified treatment of properties;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 23:36:33 +0200 |
wenzelm |
explicit mixfix block properties;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 22:35:41 +0200 |
wenzelm |
more language markup;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 19:25:04 +0200 |
wenzelm |
more PIDE markup;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 17:03:26 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 16:36:23 +0200 |
wenzelm |
clarified errors: more positions;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 22:22:12 +0200 |
wenzelm |
tuned messages -- more positions;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
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, 29 Mar 2015 19:24:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 23:00:53 +0200 |
wenzelm |
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 15:38:49 +0200 |
wenzelm |
prefer new-style Name.invents;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 22:40:29 +0200 |
wenzelm |
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 21:11:29 +0200 |
wenzelm |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 18:08:13 +0200 |
wenzelm |
simplified Pure syntax bootstrap;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 17:45:37 +0200 |
wenzelm |
renamed sprop "prop#" to "prop'" -- proper identifier;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 15:02:11 +0200 |
wenzelm |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
|
file |
diff |
annotate
| base
|