Wed, 11 Jul 2007 00:29:50 +0200 | wenzelm | Output.escape_malformed; | changeset | files |
Wed, 11 Jul 2007 00:29:49 +0200 | wenzelm | added escape_malformed (failsafe); | changeset | files |
Tue, 10 Jul 2007 23:29:53 +0200 | wenzelm | Basic editing of theory sources. | changeset | files |
Tue, 10 Jul 2007 23:29:52 +0200 | wenzelm | tuned; | changeset | files |
Tue, 10 Jul 2007 23:29:51 +0200 | wenzelm | export html_mode, begin_document, end_document; | changeset | files |
Tue, 10 Jul 2007 23:29:49 +0200 | wenzelm | renamed XML.Rawtext to XML.Output; | changeset | files |