src/Pure/ROOT.ML
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-02-10 wenzelm 2014-02-10 seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
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-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
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-11-16 wenzelm 2013-11-16 toplevel function "use" refers to raw ML bootstrap environment;
2013-09-18 wenzelm 2013-09-18 updated to polyml-5.5.1;
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
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-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
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-30 wenzelm 2013-07-30 recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
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 more uniform Counter in ML and Scala;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-05-28 wenzelm 2013-05-28 explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;
2013-05-25 haftmann 2013-05-25 tuned structure
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-17 wenzelm 2013-05-17 event timer as separate service thread;
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-12 wenzelm 2013-05-12 support for system options as context-sensitive config options;
2013-05-11 wenzelm 2013-05-11 removed redundant modules;
2013-04-03 wenzelm 2013-04-03 additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-02-25 wenzelm 2013-02-25 tuned order of modules;
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-07 wenzelm 2013-01-07 slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
2013-01-02 wenzelm 2013-01-02 moved files;
2012-12-13 wenzelm 2012-12-13 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;
2012-12-12 wenzelm 2012-12-12 support dialog via document content;
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-10-16 wenzelm 2012-10-16 more friendly handling of Pure.thy bootstrap errors;
2012-09-25 wenzelm 2012-09-25 separate module Graph_Display; tuned signature;
2012-09-25 wenzelm 2012-09-25 added graph encode/decode operations; tuned signature;
2012-08-31 wenzelm 2012-08-31 more informative error message from failed goal forks (violating old-style TTY protocol!);
2012-08-28 wenzelm 2012-08-28 discontinued centralistic changelog;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-22 wenzelm 2012-08-22 clarified bootstrapping of Pure;