fixed utterly wrong print mode handling

new serializer interface

added new code_datatype example

proper use of the Pretty module

permissive wrt. instantiation of class operations

proper lemma [source] antiquotation

check for illegal merge of class parameters

proper NoSubsort CLASS_ERROR

tuned theorem order

inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;

updated generated file;

added local_theory command wrappers;

uniform treatment of target, not as config;

more uniform treatment of OuterSyntax.local_theory commands;

updated generated file;

invisible comment;

function: uniform treatment of target, not as config;

added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;

exported master_directory;

present_excursion: setmp_thread_position during presentation;

use: explicit .ML;

ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;

fixed improper handling of return code (pdf and ps.gz formats)

add constants: set Markup.theory_nameN in tags;

added theory_nameN;

rearranged subsections

Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.

Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.

temporary adjustment

tuned