src/Pure/ROOT.ML
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;
2012-08-21 wenzelm 2012-08-21 more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-08-11 wenzelm 2012-08-11 clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
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-23 wenzelm 2012-07-23 added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
2012-07-21 wenzelm 2012-07-21 some actual build function on ML side; further imitation of "usedir" shell script;
2012-05-24 wenzelm 2012-05-24 simplified Poly/ML setup -- 5.3.0 is now the common base-line;