identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;

rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;

support dialog via document content;

merged

further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"

better tautology check -- don't reject "prod_cases3" for example

tuned debugging file names

more systematic identifier variants to facilitate experimentation;

prevent dedicated MacOSX plugin from switching off vital workarounds;

improved coupling of zoom_box and scale; explicit rescale(1.0) on startup;

really all facts means really all facts (well, almost)

tuning

use modern SAT solvers with modern Kodkod versions

got rid of support for Kodkodi < 1.2.14

made MaSh evaluation driver work with SMT solvers

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

better name for SMT solver files

updated version of MaSh learner engine

push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

disable Find_Unused_Assms_Examples for now, to recover isatest sanity;

less massive arrow heads;

added explicit zoom box;

some attempts at more discrete scale factor;

more official graphics context with font metrics;

just one class with parameters;

initial layout coordinates more like old browser; tuned geometry defaults;

added speculative options for jEdit;

separate instance of class Parameters for each Main_Panel -- avoid global program state; misc tuning;

discontinued long names flag -- better done via entity markup, without affecting layout;

tuned;

tuned;

tuned min/max;

tuned;

keep diagnostic command -- avoid confusion when it disappears;

tuned;

tuned signature;

removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;

merge

merged

merge

changed capitalization of MeSh filter

(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores

further clarification for Windows;

merged

more generous tracing limit -- rescaled in MB;

recovered title property from bfb5964e3041;

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;