proper default for max_threads; proper warmup example;

a proof of concept for generic conversions

proper name (amending 742d94015918);

invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);

avoid odd PIDE markup, notably in kokodi input;

clarified names;

clarified signature;

clarified signature;

proper treatment of timeout: <= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;

proper treatment of absolute deadline vs. relative timeout;

clarified session: no parent image for minor theory imports;

removed obsolete created_temp_dir: ISABELLE_TMP is always present for the running Isabelle/ML process;

more lemmas

proper syntax declaration

merged

reversing all the lex crap

tuned;

merged

preload library;

update to kodkodi-1.5.4-1;

clarified signature;

more realistic kodkod invocation, imitating command-line tool;

update to kodkodi-1.5.4; more realistic kodkod invocation;

rudiments of Scala interface for Kodkod;

updated to kodkodi-1.5.3: include KODKODI_CLASSPATH for Isabelle/Scala;

basic integration of Zipperposition 2.0

tuned Mirabelle comments

two more lex fixes

more lex fixes

Another go with lex: now lexordp back in class ord

List_Lexorder finally working

lexicographic ordering: new simp setup to prioritise the simpler "less_than" case

merged

fixed for new lex-order. And the effing indentation!

merged

S Holub's proposed generalisation of the lexicographic product of two orderings

allow user-defined server commands via isabelle_scala_service;

more systematic support for special directories;

proper init of cumulative settings;

upgrade phabricator: Promote 2020 Week 31 + subsequent change; upgrade arcanist: Promote 2020 Week 29;

clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");

proper protocol init (amending 065dcd80293e);

clarified names;

provide protocol handlers via isabelle_system_service;

prefer formal name;

clarified signature;

misc tuning;

clarified demo functions;

clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;

more documentation;

support JVM runtime statistics;

clarified worker threads;

misc tuning, based on hints by IntelliJ IDEA;

clarified GUI;

tuned GUI;

tuned GUI;

clarified order for GUI;

tuned;

clarified GUI;

show GC progress as "ML cleanup";

ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory;

support for Poly/ML memory status;

clarified signature;

removed pointless option "ML_statistics": always enabled;

removed pointless GUI controls for ML_statistics --- no longer part of prover protocol (see also 38a64cc17403);

support for GC state;

updated to polyml-test-f54aa41240d0;

back to polyml-5.8.1 due to ML compiler crash in HOL-Codegenerator_Test;

updated to polyml-test-159dc81efc3b;

dedicated symbols for code generation, to pave way for generic conversions from and to word

consolidated names

reduced prominence od theory Bits_Int

one last lemma about Total and Restr

adjustments for fewer WO assumptions

elimination of some needless assumptions

merged

iso lemmas

tuned

tuned

NEWS;

provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);

adapted to 7b318273a4aa;

cache props;

clarified names; removed remains of old protocol messages;

more thorough protocol_handlers.exit, like file_formats.stop_session;

tuned names;

temporary workaround for 100% CPU usage in OS.Process.sleep;

ML statistics via external process: allows monitoring RTS while ML program sleeps;

clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;

avoid failure of "isabelle build -o skip_proofs";

merged

recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document at ..." (see also 940195fbb282, 5469bacf5573, 5c4800f6b25a);

more compact command_timings, as in former batch-build;

unused;

unused --- superseded by PIDE messages;

more thorough cleanup, e.g. before ML_Heap.save;