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;

less excessive event handling;

tuned;

clarified mouse wheel: conventional scrolling, not scaling;

clarified metrics, similar to old graph browser;

merged

tuned color;

tuned signature;

tuned signature;

more dynamic visualizer -- re-use jEdit font info;

tuned signature;

tuned signature;

more dynamic visualizer -- re-use Isabelle/jEdit options; clarified iTextField error: like Isabelle/jEdit search field; tuned signature;

more standard GUI layout;

tuned;

tuned imports;

tuned;

tuned imports;

tuned signature;

tuned signature;

tuned signature;

tuned;

tuned whitespace;

merged

updated NEWS

optionally display statistics for Z3 proof reconstruction

avoid more than one data slot per module

limit reconstruction time of Z3 proof steps to be able to detect long-running reconstruction steps

converse graph according to Graph_Display;

eliminated TTY/PG legacy;

clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned;

tuned;

for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes

more explict and generic field names

uniform variable name for presentation graphs, to distinguish from values of type Graph.T

stripped ad-hoc diagnostic facility

update map definition in Prog_Prove for new datatype package

explicit message channel for "legacy", which is nonetheless a variant of "warning";

clarified source location;

added system property isabelle.laf, notably for initial system dialog; let L&F take care of font scaling, e.g. GTK+ for Linux where X11 dpi scaling does not really work;

NEWS;

tuned;

clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;

tuned whitespace;

more toplevel pretty printing;

back to full synchronization (cf. eb3e399f5b9f);

proper sequential version;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;

modernized historic example;

more thorough Lazy.is_finished;

3 old example lemmas by Amine listed in the top 100 theorems

update_cartouches; trimmed whitespace;

memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

typos

unused;

tuned message;

explicit message channels for "state", "information"; separate state_message_color;

imitate font more carefully: err on smaller size; imitate HTML font, notably for Sidekick where short string is also shown as view status message;

more accurate selection of sessions;

more accurate selection of sessions;

discontinued central critical sections: NAMED_CRITICAL / CRITICAL;

more elementary Multithreading.synchronized;

proper Synchronized.var; more atomic operations;

removed remains from Proof General;

obsolete;

system option "pretty_margin" is superseded by "thy_output_margin";

tuned;

proper Synchronized.var;

separate module Random; proper Synchronized.var;

tuned;

tuned signature;

proper context;

afford more heap;

increase chances of success;

recovered metis proof after 115965966e15 (Odd clash of type variables!?);

proper context;

proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;

tuned;

afford full test, with slightly improved scheduling order;

more generous timeout, to increase chances of at64-poly;

updated according to eb3e399f5b9f;

just one data slot per program unit; tuned signature;

tuned;

just one data slot per program unit; tuned signature;

more standard configuration options;

tuned;

just one data slot per program unit;

tuned;

more frugal Local_Syntax.init -- maintain idents within context;

proper exception for internal program failure, not user-error;

tuned;

suppress irrelevant timing messages (the majority);

less ambitious settings -- increase chances of success;

peek value without synchronization;

avoid repeated access to global variable (101 times in Complex_Main), which is actually synchronized after e557a9ddee5f;

tuning

unfortunately, there is no general function space in the measurable spaces

correctly apply type substitution before checking for function types

avoid generating selectors with function types -- this produce arity inconsistencies

renamed theory file

merged

Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);

tuned;

tuned;

added Par_List in Scala, in accordance to ML version; system property "isabelle.threads" determines size of Scala thread pool, like system option "threads" for ML; avoid ".par" framework with its hard-wired thread pool, which also has problems with cancellation; tuned;

tuned;

rel_pmf commutes with rel_prod

note more facts (always)

conceal typedef more violently

respect order of deads when retrieving bnfs from the database

merged

more informative gutter content: fall-back on background color, e.g. when line numbers are enabled; non-transparent information_message_color like other message colors; removed unused error1_color;

more examples;

more careful handling of auxiliary environment structure -- allow nested ML evaluation;