src/Pure/General/output.ML
2014-08-15 wenzelm 2014-08-15 explicit system message for protocol failure -- show on Syslog panel instead of Raw Output; more robust crash recovery: warning could crash again;
2014-05-02 wenzelm 2014-05-02 tuned signature -- channels for diagnostic output for system tools means stderr;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-31 wenzelm 2014-03-31 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2014-03-27 wenzelm 2014-03-27 redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;
2014-03-26 wenzelm 2014-03-26 support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);
2014-02-10 wenzelm 2014-02-10 seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
2013-11-11 wenzelm 2013-11-11 tuned signature;
2013-09-04 wenzelm 2013-09-04 some explicit indication of Proof General legacy;
2013-08-02 wenzelm 2013-08-02 more general Output.result: allow to update arbitrary properties; clarified kind/instance of overlay GUI component, with separate output (subject to version as main Output);
2013-08-02 wenzelm 2013-08-02 tuned signature;
2013-04-09 wenzelm 2013-04-09 clarified protocol_message undefinedness;
2012-12-13 wenzelm 2012-12-13 smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13 wenzelm 2012-12-13 enable Isabelle/ML to produce uninterpreted result messages as well;
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-05-25 wenzelm 2012-05-25 ignore empty messages even on tty, e.g. relevant for Isabelle_System.bash_output err output;
2012-03-03 wenzelm 2012-03-03 clarified terminology of raw protocol messages;
2011-08-27 wenzelm 2011-08-27 explicit markup for legacy warnings;
2011-08-23 wenzelm 2011-08-23 tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-07-11 wenzelm 2011-07-11 made SML/NJ happy; tuned error;
2011-07-11 wenzelm 2011-07-11 JVM method invocation service via Scala layer;
2011-07-11 wenzelm 2011-07-11 some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;
2011-07-06 wenzelm 2011-07-06 prefer Synchronized.var;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2010-10-25 wenzelm 2010-10-25 more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-25 wenzelm 2010-10-25 explicitly qualify type Output.output, which is a slightly odd internal feature;
2010-10-25 wenzelm 2010-10-25 removed some remains of Output.debug (follow-up to fce2202892c4);
2010-09-27 wenzelm 2010-09-27 renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-08-28 wenzelm 2010-08-28 non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;
2010-08-27 wenzelm 2010-08-27 discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-12 wenzelm 2010-07-12 removed impractical tolerate_legacy_features flag;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-17 wenzelm 2009-06-17 removed obsolete time accumulator (better use Toplevel.profiling);
2009-03-23 wenzelm 2009-03-23 removed obsolete ml_output;
2009-03-23 wenzelm 2009-03-23 suppress status output for traditional tty modes (including Proof General); keyword report: explicitly issue message on writeln channel as well;
2009-03-06 wenzelm 2009-03-06 eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-01 wenzelm 2009-03-01 end_timing: generalized result -- message plus with explicit time values;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-07-15 wenzelm 2008-07-15 added status channel; writeln_default: suppress empty messages;
2008-03-15 wenzelm 2008-03-15 tuned messages;
2008-01-06 wenzelm 2008-01-06 added explicit prompt channel (prompt_fn/prompt); tuned;
2007-12-17 wenzelm 2007-12-17 cond_timeit: added message argument, use Exn.capture/release; tuned;
2007-12-17 haftmann 2007-12-17 tuned
2007-12-17 haftmann 2007-12-17 improved semantics of timeapp_msg
2007-12-15 wenzelm 2007-12-15 removed unused escape_malformed;
2007-09-19 wenzelm 2007-09-19 ml_output: proper error instead of error_msg;
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-07-29 wenzelm 2007-07-29 NAMED_CRITICAL;
2007-07-29 wenzelm 2007-07-29 removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-19 wenzelm 2007-07-19 tuned;
2007-07-11 wenzelm 2007-07-11 added escape_malformed (failsafe);
2007-07-09 wenzelm 2007-07-09 type output = string indicates raw system output;
2007-07-07 wenzelm 2007-07-07 renamed raw to escape; simplified pretty token metric: type int; simplified print_mode setup: output_width and escape; moved pretty setup to pretty.ML;