proper check for active server;

clarified signature;

tuned signature;

handle server connections;

clarified database names;

more options; misc tuning and clarification;

support for resident Isabelle servers;

default according to Java API, instead of jEdit usage;

do not fall back on nbe if plain evaluation fails

final tidying up of lemma bounded_variation_absolutely_integrable_interval

finally rid of finite_product_dependent

more cleanup

trying to disentangle bounded_variation_absolutely_integrable_interval

merged

more horrible proofs disentangled

tuned

more structural sharing between common target Generic_Target.init

exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements

treat exit separate from regular local theory operations

provide explicit variant initializers for regular named target vs. almost-named target

prefer explicit datatype over implicit sum; given up separate implementation to pretty-print locale specifications

compactified output

lifting setup for char

one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy

uniform namespace handling for both concrete and abstract types, following 32e0da92c786

clarified

corrected slip

tuned

work around weakness in export calculation when generating OCaml code

tuned