src/Pure/Syntax/syntax.ML
Tue, 13 Aug 2019 21:18:26 +0200 wenzelm minor performance tuning;
Tue, 30 Jul 2019 11:41:39 +0200 wenzelm clarified modules;
Sun, 24 Mar 2019 19:17:42 +0100 wenzelm clarified markup;
Thu, 03 Jan 2019 21:48:05 +0100 wenzelm support for isabelle update -u inner_syntax_cartouches;
Thu, 03 Jan 2019 15:55:36 +0100 wenzelm tuned signature;
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Fri, 28 Sep 2018 22:33:20 +0200 wenzelm more accurate syntax: e.g. avoid brackets as prefix notation;
Fri, 28 Sep 2018 21:16:24 +0200 wenzelm more approximative prefix syntax, including binder;
Wed, 26 Sep 2018 17:04:50 +0200 wenzelm clarified get_infix: avoid old ASCII input syntax;
Sun, 16 Sep 2018 22:45:34 +0200 wenzelm export plain infix syntax;
Sun, 16 Sep 2018 20:33:37 +0200 wenzelm unused;
Sat, 27 Jan 2018 16:56:03 +0100 wenzelm prefer lazy update;
Sat, 27 Jan 2018 16:45:27 +0100 wenzelm tuned output;
Thu, 22 Jun 2017 15:20:32 +0200 wenzelm more informative task_statistics;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Wed, 22 Jun 2016 10:42:53 +0200 wenzelm tuned;
Thu, 07 Apr 2016 12:08:02 +0200 wenzelm prefer regular context update, to allow continuous editing of Pure;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Sun, 29 Mar 2015 19:24:07 +0200 wenzelm tuned signature;
Tue, 24 Mar 2015 11:53:18 +0100 wenzelm clarified input source;
Sun, 30 Nov 2014 12:24:56 +0100 wenzelm more abstract type Input.source;
Wed, 12 Nov 2014 18:18:38 +0100 wenzelm prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
Tue, 11 Nov 2014 18:16:25 +0100 wenzelm more position information, e.g. relevant for errors in generated ML source;
Wed, 27 Aug 2014 12:32:42 +0200 wenzelm tuned signature -- prefer quasi-abstract Symbol_Pos.source;
Sun, 06 Apr 2014 16:36:28 +0200 wenzelm more source positions;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Sat, 01 Mar 2014 23:17:37 +0100 wenzelm tuned signature;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Sun, 26 May 2013 20:42:43 +0200 wenzelm tuned signature;
less more (0) -100 -50 -30 tip