Sat, 29 May 2004 15:06:19 +0200 | wenzelm | improved support for raw symbols; | changeset | files |
Sat, 29 May 2004 15:06:04 +0200 | wenzelm | Output.error; | changeset | files |
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; | changeset | files |