discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;

tuned;

added lemma

typo

avoid writing into source

clarified active_job: take dependencies into account (e.g. future based on promise);

tuned;

non-strict print_state: display old proof state on failure, e.g. unfinished command;

permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;

clarified Event_Timer.shutdown: manager thread remains until final shutdown in Session.finish; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

ignore print process even after fork, to avoid loosing active worker threads;

rel_pmf OO: conversion to nat is not necessary

merged

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;