some clarification for Windows;

stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;

tuned;

generalized notion of active area, where sendback is just one application; some support for graphview via active area;

merged

have MaSh evaluator keep all raw problem/solution files in a directory

clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;

always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);

added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

merged

merge

don't blacklist "case" theorems -- this causes problems in MaSh later

more changes to MaSh Python program (by Daniel K.)

don't have MaSh pretend it knows facts it doesn't know

reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)

fixed embarrassing off-by-one bug in MaSh's Mesh

store evaluation output in a file

use parallel map

tweak MaSh fudge factors

more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"

basic monitor panel, using the powerful jfreechart library; sorted Isabelle menu entries -- this is mainly a catalog;

added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);

check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);

make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);

final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;

adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;

obsolete;

eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005); \usepackage{proof} only where required;

merged

deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;

some support to recover from spurious crash -- this is Physics, not Mathematics;

avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;

tuned text

corrected nonsensical associativity of `` and dvd

add exponential and uniform distributions

fundamental theorem of calculus for the Lebesgue integral

add Int_atMost

more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;

fork slow part of Thy_Load.body_files only;

explore theory_body_files via future, for improved performance; further internalization of header errors;

merged

use proper entry point for MaSh in test driver

export ATP and Isar commands separately

proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);

discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;

discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;

updated README;

documentation for isabelle build_dialog and its implicit use in isabelle jedit;

clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL); added jedit option -n to bypass build_dialog;

avoid startup within GUI thread -- it is only required later for dialog; tuned signature;

more uniform default logic, using settings, options, args etc.; clarified build_dialog -C: imitate jEdit logic selection more precisely;

use right names in MePo exporter

parse more liberal MaSh suggestion syntax (for the eval driver)

merged

made Python code compile again (by Daniel K.)

tweaked MaSh proximity