| Mon, 20 Jun 2022 16:15:07 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 20:01:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 13:37:15 +0100 |
wenzelm |
back to more elementary Buffer.T -- less intermediate garbage;
|
file |
diff |
annotate
|
| Wed, 21 Aug 2019 17:32:44 +0200 |
wenzelm |
more scalable: avoid huge intermediate XML elems;
|
file |
diff |
annotate
|
| Wed, 21 Aug 2019 15:19:31 +0200 |
wenzelm |
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 15:05:45 +0200 |
wenzelm |
more scalable;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 13:41:53 +0200 |
wenzelm |
precise BinIO, without newline conversion on Windows;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 22:42:08 +0100 |
wenzelm |
removed unused add_substring;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 20:36:26 +0200 |
wenzelm |
renamed Buffer.write to File.write_buffer;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 21:23:36 +0200 |
wenzelm |
output: canonical argument order (as opposed to write);
|
file |
diff |
annotate
|
| Mon, 31 Mar 2008 23:08:53 +0200 |
wenzelm |
added add_substring;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:47 +0200 |
wenzelm |
added markup operation;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:54 +0200 |
wenzelm |
removed obsolete Library.seq;
|
file |
diff |
annotate
|
| Sun, 03 Dec 2006 23:21:55 +0100 |
aspinall |
Add output function
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:47 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:33 +0200 |
wenzelm |
tuned Buffer.add;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 10:41:46 +0200 |
wenzelm |
tuned write: use File.write_list;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:02:46 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 12:19:21 +0200 |
wenzelm |
removed write_nonempty;
|
file |
diff |
annotate
|
| Wed, 06 Oct 1999 18:11:37 +0200 |
wenzelm |
added write_nonempty;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:08:50 +0100 |
wenzelm |
simple string buffers;
|
file |
diff |
annotate
|