| Wed, 11 Sep 2024 12:46:56 +0200 |
wenzelm |
revert 90f6e541e926, which has become pointless thanks to df85df6315af;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2024 12:32:11 +0200 |
wenzelm |
clarified signature and modules;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2024 20:06:51 +0200 |
wenzelm |
clarified signature, roughly following Isabelle/Scala;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2024 23:50:58 +0200 |
wenzelm |
minor performance tuning, following Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2024 20:31:20 +0200 |
wenzelm |
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| Mon, 02 Sep 2024 20:54:00 +0200 |
wenzelm |
clarified modules: enable pretty.ML to use XML/YXML more directly;
|
file |
diff |
annotate
|
| Mon, 02 Sep 2024 15:23:12 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 31 Aug 2024 16:00:16 +0200 |
wenzelm |
minor performance tuning: avoid many small strings, notably in File_Stream.output;
|
file |
diff |
annotate
|
| Mon, 01 Jul 2024 12:37:03 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Mon, 15 Nov 2021 11:38:14 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Nov 2021 20:15:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 20:01:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 22:18:37 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 10 Apr 2021 21:50:59 +0200 |
wenzelm |
more robust treatment of empty markup: it allows to produce formal chunks;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 13:25:58 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 12:33:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 12:02:27 +0100 |
wenzelm |
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 16:51:47 +0200 |
wenzelm |
more compact XML representation;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2019 15:45:34 +0100 |
wenzelm |
tuned according to Scala version;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2019 14:44:41 +0100 |
wenzelm |
uniform XML header;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 12:34:26 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2018 21:10:55 +0100 |
wenzelm |
tuned signature (see also src/Tools/Haskell/Markup.hs);
|
file |
diff |
annotate
|
| Sun, 04 Nov 2018 17:19:56 +0100 |
wenzelm |
more Haskell operations;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2018 19:31:50 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2017 15:37:14 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2016 23:11:00 +0200 |
wenzelm |
clarified modules;
|
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
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2015 22:35:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 13:41:53 +0200 |
wenzelm |
precise BinIO, without newline conversion on Windows;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 14:17:13 +0100 |
wenzelm |
some document antiquotations for Isabelle/jEdit elements;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 22:53:18 +0200 |
wenzelm |
support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 19:50:10 +0200 |
wenzelm |
discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 17:40:33 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 29 Mar 2012 22:43:50 +0200 |
wenzelm |
more specific notion of partiality (cf. Scala version);
|
file |
diff |
annotate
|
| Thu, 08 Mar 2012 21:40:15 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Thu, 08 Mar 2012 21:36:36 +0100 |
wenzelm |
simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
|
file |
diff |
annotate
|
| Thu, 08 Mar 2012 19:56:57 +0100 |
wenzelm |
clarified XML signature (again) -- coincide with basic Markup without explicit dependency;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 16:56:01 +0200 |
wenzelm |
slightly more standard-conformant XML parsing (see also 94033767ef9b);
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 00:20:09 +0200 |
wenzelm |
more substructural sharing to gain significant compression;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 23:08:04 +0200 |
wenzelm |
XML.cache for partial sharing (strings only);
|
file |
diff |
annotate
|
| Sun, 04 Sep 2011 15:21:50 +0200 |
wenzelm |
moved XML/YXML to src/Pure/PIDE;
|
file |
diff |
annotate
| base
|