src/Pure/ROOT.ML
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;
2012-05-24 wenzelm 2012-05-24 discontinued support for Poly/ML 5.2.1;
2012-04-27 wenzelm 2012-04-27 made Context_Position independent from Config;
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution;
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations;
2011-12-01 wenzelm 2011-12-01 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
2011-11-29 wenzelm 2011-11-29 clarified modules;
2011-11-29 wenzelm 2011-11-29 rearranged files;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-11-19 wenzelm 2011-11-19 added ML antiquotation @{attributes};
2011-09-23 wenzelm 2011-09-23 discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
2011-09-22 wenzelm 2011-09-22 abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;
2011-09-21 wenzelm 2011-09-21 slightly more general Socket_IO as part of Pure;