allow line breaks in integral notation

allow line breaks in probability syntax

don't minimize chained facts -- this leads to subtle failures, e.g. if a method succeeds without a chained fact but fails with it

NEWS

measurability prover: removed app splitting, replaced by more powerful destruction rules

tuned warnings: observe Context_Position.is_visible;

removed unused/non-portable with_tmp_fifo;

discontinued fifo channel, always use portable socket;

tuned -- more Sidekick-friendly layout;

do not crash into already running exec, instead join its lazy result in the subsequent step (amending 59f1591a11cb);

more explicit errors;

proper latex;

tuned -- less redundant;

proper Session.save with shutdown, which is relevant to avoid persistent threads;

tuned latex;

merged

always use socket to test performance and stability;

explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

tuned;

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;