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;

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

remove duplication in tactic

document 'case_distrib'

tuning

generate 'case_distrib' for Ctr_Sugars

more metrics, with integer coordinates for layout; initial coordinates: center x as in old browser; Layout.pendulum/collapse: proper downwards range; distance as in old browser (see spaceBetween); move offset as in old browser; more careful comparison wrt. 0.0 (this is IEEE double, not int);

tuned;

misc tuning;

explicit Layout.Point; tuned signature; tuned;

tuned comments;

tuned;

clarified static full_graph vs. dynamic visible_graph; tuned;

tuned signature;

tuned -- more iterators;

tuned;

clarified fit_to_window: floor scale within window bounds;

tuned;

apply_layout: proper repaint; discontinued dysfunctional keyboard interaction: avoid delicate questions about focus and "standard" key bindings in Isabelle/jEdit;

tuned;

tuned;

tuned;

tuned;

tuned signature;

tuned menu items;

tuned signature;

more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;

more uniform support for graph display in ML/Scala;

recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;

prefer integer coordinates; tuned painting;

clarified bounding box, similar to old graph browser; default font like old browser; clarified metrics; tuned signature;

tuned headers;