clarified worker threads;

support JVM runtime statistics;

misc tuning, based on hints by IntelliJ IDEA;

clarified GUI;

tuned GUI;

tuned GUI;

clarified order for GUI;

tuned;

clarified GUI;

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

show GC progress as "ML cleanup";

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…

support for GC state;

updated to polyml-test-f54aa41240d0;

Functions marked as InlineAlways can be recursive and so the inline marking has…

Use config.h for the Windows osmem if it is provided e.g. by Msys.

updated to polyml-test-159dc81efc3b;

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

Remake Makefile.in after merge.

Merge branch 'ExecuteWrite'

Merge branch 'master' into ExecuteWrite

Use O_TMPFILE on Linux to create the temporary file for mapping. Saves having…

Add MAP_STACK in 32-in-64 for OpenBSD.

Support 32-in-64 on OSs that disallow write+execute.

Fix changes for Unix.

Split the Windows and Unix versions of the allocators.

Merge branch 'ExecuteWrite' of https://github.com/dcjm/polyml into ExecuteWrite

Should be @progbits not %.

Add an extra section when exporting on Linux to mark the stack as non…

Remove the configure test for the non-executable stack flag and instead use it…

Merge branch 'ExecuteWrite' of https://github.com/dcjm/polyml into ExecuteWrite

Fixes to compile on Linux.

Mmap with execute+write returns EACCES in SElinux.

Change from boolean executable/non-executable into a three-way selection…

Implement dual areas if mmap fails when write+execute permission is requested.

When trying to write to the code area write to the shadow area instead. This…

The interpreted version does not need "code" to have execute permission because…

Change osmem.cpp for Linux.

Change the low-level allocator to separate out code and data allocation.

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

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

consolidated names

reduced prominence od theory Bits_Int

merged

more on order types

one last lemma about Total and Restr

adjustments for fewer WO assumptions

elimination of some needless assumptions

merged

iso lemmas

Merge branch 'master' into GCPercent

tuned

tuned

Add Phil's test as a regression test.

Mark inline shim functions generated by the optimiser differently from those…

Poll should still pause if there are no descriptors. Fix problem with OS.

NEWS;

provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127…

adapted to 7b318273a4aa;

cache props;

clarified names;

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…

clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt…

Some clean up of remote statistics in Windows.

The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if…

avoid failure of "isabelle build -o skip_proofs";

merged

recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document…

more compact command_timings, as in former batch-build;

unused;

unused --- superseded by PIDE messages;

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

discontinued old batch-build functionality;

dropped alias

tailored towards remaining essence

Posix.Process.exit should call PolyFinish rather than PolyTerminate so that…

Tidy-up shutdown of statistics.

Fix changes to statistics.cpp for Windows.

Unlink any existing statistics file. Open will fail if it exists. Report an…

merged

added theory Tree23_of_List

tuned

more robust treatment of thm_names, with strict check after all theories are…

a few more lemmas

Small change to 8e4d341 to allow compilation when int is IntInf.int.

merged

yet another little lemma

lemmas about sets and the enumerate operator

merged

merged

merged

strengthened a lemma

A new lemma about abstract Sum / Prod