src/Pure/ROOT
2014-09-29 wenzelm 2014-09-29 pro-forma support for polyml-5.5.3 (presently SVN 1960);
2014-08-19 wenzelm 2014-08-19 clarified modules;
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-06 wenzelm 2014-04-06 approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
2014-03-11 wenzelm 2014-03-11 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2014-02-16 wenzelm 2014-02-16 prefer user-space tool within Pure.thy;
2014-01-25 wenzelm 2014-01-25 prefer self-contained user-space tool;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;
2013-12-12 wenzelm 2013-12-12 simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
2013-12-11 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-09-18 wenzelm 2013-09-18 moved module into plain Isabelle/ML user space;
2013-08-26 wenzelm 2013-08-26 added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
2013-08-08 wenzelm 2013-08-08 removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
2013-08-05 wenzelm 2013-08-05 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
2013-08-01 wenzelm 2013-08-01 exception trace for Poly/ML 5.5.1, using regular Isabelle output;
2013-07-19 wenzelm 2013-07-19 old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
2013-07-12 wenzelm 2013-07-12 clarified module name;
2013-07-11 wenzelm 2013-07-11 global management of command execution fragments; tuned;
2013-07-10 wenzelm 2013-07-10 more abstract message channel;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-05-28 wenzelm 2013-05-28 explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;
2013-05-17 wenzelm 2013-05-17 event timer as separate service thread;
2013-05-15 wenzelm 2013-05-15 tuned;
2013-05-15 wenzelm 2013-05-15 moved files;
2013-05-15 wenzelm 2013-05-15 maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;
2013-05-15 wenzelm 2013-05-15 just one ProofGeneral module;
2013-05-14 wenzelm 2013-05-14 simplified modules and exceptions;
2013-05-13 wenzelm 2013-05-13 more direct output of remaining PGIP rudiments;
2013-05-13 wenzelm 2013-05-13 removed obsolete PGIP material;
2013-05-11 wenzelm 2013-05-11 removed redundant modules;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-11 wenzelm 2013-03-11 support for 'chapter' specifications within session ROOT;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-10 wenzelm 2013-01-10 recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
2013-01-02 wenzelm 2013-01-02 moved files;
2012-12-10 wenzelm 2012-12-10 generalized notion of active area, where sendback is just one application; some support for graphview via active area;
2012-11-28 wenzelm 2012-11-28 some support for ML runtime statistics;
2012-11-26 wenzelm 2012-11-26 clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-11-22 wenzelm 2012-11-22 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
2012-09-25 wenzelm 2012-09-25 separate module Graph_Display; tuned signature;
2012-08-24 wenzelm 2012-08-24 clarified syntax boundary cases and errors;
2012-08-22 wenzelm 2012-08-22 clarified bootstrapping of Pure;
2012-08-08 wenzelm 2012-08-08 simplified session specifications: names are taken verbatim and current directory is default;
2012-08-08 wenzelm 2012-08-08 simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
2012-08-05 wenzelm 2012-08-05 prefer general Command_Line.tool wrapper (cf. Scala version);
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure outer syntax;
2012-07-26 wenzelm 2012-07-26 more files for session Pure;
2012-07-22 wenzelm 2012-07-22 determine source dependencies, relatively to preloaded theories; tuned signature;
2012-07-19 wenzelm 2012-07-19 more explicit treatment of initial Pure sessions;