| Tue, 09 May 2023 23:56:40 +0200 |
wenzelm |
backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons;
|
file |
diff |
annotate
|
| Tue, 09 May 2023 21:50:04 +0200 |
wenzelm |
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
|
file |
diff |
annotate
|
| Tue, 09 May 2023 21:32:03 +0200 |
wenzelm |
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
|
file |
diff |
annotate
|
| Thu, 08 Sep 2022 12:52:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 21:18:26 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 11:41:39 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 19:17:42 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:48:05 +0100 |
wenzelm |
support for isabelle update -u inner_syntax_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 15:55:36 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 22:33:20 +0200 |
wenzelm |
more accurate syntax: e.g. avoid brackets as prefix notation;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2018 21:16:24 +0200 |
wenzelm |
more approximative prefix syntax, including binder;
|
file |
diff |
annotate
|
| 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
|
| Sun, 16 Sep 2018 20:33:37 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 27 Jan 2018 16:56:03 +0100 |
wenzelm |
prefer lazy update;
|
file |
diff |
annotate
|
| Sat, 27 Jan 2018 16:45:27 +0100 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 15:20:32 +0200 |
wenzelm |
more informative task_statistics;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:42:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 12:08:02 +0200 |
wenzelm |
prefer regular context update, to allow continuous editing of Pure;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 19:24:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 12:32:42 +0200 |
wenzelm |
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 16:36:28 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 23:17:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 20:42:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
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
|
| Fri, 29 Mar 2013 22:14:27 +0100 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
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
|
| Mon, 01 Oct 2012 16:37:22 +0200 |
wenzelm |
report sort assignment of visible type variables;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 13:06:23 +0100 |
wenzelm |
added Syntax.read_typs;
|
file |
diff |
annotate
|
| Fri, 09 Mar 2012 20:04:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 15:42:26 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Mon, 16 Jan 2012 21:50:15 +0100 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 20:26:01 +0100 |
wenzelm |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
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
|
| Fri, 25 Nov 2011 23:04:12 +0100 |
wenzelm |
removed obsolete argument (cf. 954e9d6782ea);
|
file |
diff |
annotate
|
| Fri, 25 Nov 2011 16:32:29 +0100 |
wenzelm |
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 17:48:26 +0100 |
wenzelm |
inner syntax positions for string literals;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 14:58:48 +0100 |
wenzelm |
tuned signature -- emphasize internal role of these operations;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:05:53 +0200 |
wenzelm |
explicit join_syntax ensures command transaction integrity of 'theory';
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
file |
diff |
annotate
|
| Sat, 06 Aug 2011 15:48:08 +0200 |
kleing |
make syntax ambiguity warnings a config option
|
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
|
| Mon, 27 Jun 2011 15:01:08 +0200 |
wenzelm |
parallel Syntax.parse, which is rather slow;
|
file |
diff |
annotate
|
| Sun, 15 May 2011 22:22:26 +0200 |
wenzelm |
future merge of grammars, to improve parallel performance;
|
file |
diff |
annotate
|