simplify construction for distribution of rel_pmf over op OO

prefer option for default code printing width

modernized and more uniform style

tuned order

tuned

avoid technical term "mixin" in user documentation text

tuned;

merged

updated bibtex

tuned;

misc tuning;

made SML/NJ happier

configurable options;

proper level distance according to number of edges, as in old browser;

clarified Vertex.Ordering, to approximate situation before 4d985afc0565, which is relevant for level arrangement;

tuned;

merged

NEWS;

rubberband method as in old browser; tuned;

tuned;

tuned signature;

proper translate vertex (cf. 4d985afc0565);

tuned signature;

explict layout graph structure, with dummies and coordinates; explicit metrics for dummy box; tuned signature; misc tuning;

tuned;

docs

docs

docs

tuning

formal pretty bodies for class specifications, accepting additional formal bookkeeping in locale.ML

merged

clarified visualizer parameters; do not show dummies by default;

tuned metrics;

proper bounding box including dummies;

more direct coordinates for dummy;

separate module Metrics; maintain static metrics (with font) and visible_graph via layout;

tuned imports;

apply layout on change of options;

avoid fractional font size;

GUI.imitate_font: more explicit result size, e.g. relevant for caching; some graphview font options: Helvetica family is important for self-contained PDF; tuned;

eliminated print modes: offer new and old graph;

docs

generate [code] only with 'code' plugin enabled

docs

added plugins syntax to prim(co)rec

docs

tuning

docs

documented 'transfer' options to 'prim(co)rec'

tuning

Add plugin to generate transfer theorem for primrec and primcorec

use proper context in function

document 'disc_eq_case'

tuning

generate 'disc_eq_case' for Ctr_Sugars

tuning