| Thu, 17 Apr 2008 16:30:48 +0200 |
wenzelm |
removed obsolete raw_str;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:49 +0200 |
wenzelm |
Buffer.markup;
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 16:45:00 +0200 |
wenzelm |
moved print_mode setup for markup to markup.ML;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:52:10 +0200 |
wenzelm |
symbolic output: avoid empty blocks, 1 space for fbreak;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 13:10:54 +0200 |
wenzelm |
export mode_markup;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:18 +0200 |
wenzelm |
added markup_chunks;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 12:16:16 +0200 |
wenzelm |
markup: emit as control information -- no indent text;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 00:14:58 +0200 |
wenzelm |
added print_mode setup: indent and markup;
|
file |
diff |
annotate
|
| Fri, 05 Jan 2007 14:31:48 +0100 |
haftmann |
added block_enclose
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:35 +0100 |
wenzelm |
added command, keyword;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:08 +0100 |
wenzelm |
renamed gen_list to enum;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:27 +0100 |
wenzelm |
added backquote;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 10:39:38 +0200 |
haftmann |
(name mess cleanup)
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 18:47:42 +0200 |
paulson |
fixed recursive-looking declaration
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 07:35:38 +0200 |
haftmann |
added gen_list to Pretty module
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 10:41:48 +0200 |
wenzelm |
added output_buffer;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Tue, 22 Jun 2004 09:51:59 +0200 |
wenzelm |
added output, removed pp_undef;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sun, 20 Jun 2004 09:26:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:05:51 +0200 |
wenzelm |
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2001 14:42:45 +0100 |
wenzelm |
added writelns;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2001 19:53:29 +0100 |
wenzelm |
support general indentation (e.g. for non-tt latex output);
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 20:13:17 +0200 |
wenzelm |
added indent;
|
file |
diff |
annotate
|
| Sun, 25 Jun 2000 23:46:22 +0200 |
wenzelm |
fbrk: 2 if not taken;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:02:46 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:18:12 +0100 |
wenzelm |
removed lst, strlen, strlen_real, spc, sym;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:11:00 +0100 |
wenzelm |
added strlen_real, setmp_margin;
|
file |
diff |
annotate
|
| Thu, 11 Feb 1999 21:15:46 +0100 |
wenzelm |
sym: Symbol.output_width;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 15:18:02 +0100 |
wenzelm |
fixed titles;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:44:33 +0100 |
wenzelm |
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
|
file |
diff |
annotate
|