| 2011-07-11 |
wenzelm |
2011-07-11 |
JVM method invocation service via Scala layer;
|
file | diff | annotate |
| 2011-07-11 |
wenzelm |
2011-07-11 |
some support for raw messages, which bypass standard Symbol/YXML decoding;
tuned signature;
|
file | diff | annotate |
| 2011-07-06 |
wenzelm |
2011-07-06 |
prefer Synchronized.var;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2010-10-25 |
wenzelm |
2010-10-25 |
more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
|
file | diff | annotate |
| 2010-10-25 |
wenzelm |
2010-10-25 |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file | diff | annotate |
| 2010-10-25 |
wenzelm |
2010-10-25 |
explicitly qualify type Output.output, which is a slightly odd internal feature;
|
file | diff | annotate |
| 2010-10-25 |
wenzelm |
2010-10-25 |
removed some remains of Output.debug (follow-up to fce2202892c4);
|
file | diff | annotate |
| 2010-09-27 |
wenzelm |
2010-09-27 |
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
|
file | diff | annotate |
| 2010-08-28 |
wenzelm |
2010-08-28 |
non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;
|
file | diff | annotate |
| 2010-08-27 |
wenzelm |
2010-08-27 |
discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;
|
file | diff | annotate |
| 2010-08-08 |
wenzelm |
2010-08-08 |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file | diff | annotate |
| 2010-07-12 |
wenzelm |
2010-07-12 |
removed impractical tolerate_legacy_features flag;
|
file | diff | annotate |
| 2009-10-17 |
wenzelm |
2009-10-17 |
indicate CRITICAL nature of various setmp combinators;
|
file | diff | annotate |
| 2009-09-29 |
wenzelm |
2009-09-29 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| 2009-06-17 |
wenzelm |
2009-06-17 |
removed obsolete time accumulator (better use Toplevel.profiling);
|
file | diff | annotate |
| 2009-03-23 |
wenzelm |
2009-03-23 |
removed obsolete ml_output;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2009-03-06 |
wenzelm |
2009-03-06 |
eliminated Output.immediate_output -- violates the official message channel protocol;
|
file | diff | annotate |
| 2009-03-01 |
wenzelm |
2009-03-01 |
end_timing: generalized result -- message plus with explicit time values;
|
file | diff | annotate |
| 2009-01-21 |
wenzelm |
2009-01-21 |
removed Ids;
|
file | diff | annotate |
| 2008-07-15 |
wenzelm |
2008-07-15 |
added status channel;
writeln_default: suppress empty messages;
|
file | diff | annotate |
| 2008-03-15 |
wenzelm |
2008-03-15 |
tuned messages;
|
file | diff | annotate |
| 2008-01-06 |
wenzelm |
2008-01-06 |
added explicit prompt channel (prompt_fn/prompt);
tuned;
|
file | diff | annotate |
| 2007-12-17 |
wenzelm |
2007-12-17 |
cond_timeit: added message argument, use Exn.capture/release;
tuned;
|
file | diff | annotate |
| 2007-12-17 |
haftmann |
2007-12-17 |
tuned
|
file | diff | annotate |
| 2007-12-17 |
haftmann |
2007-12-17 |
improved semantics of timeapp_msg
|
file | diff | annotate |
| 2007-12-15 |
wenzelm |
2007-12-15 |
removed unused escape_malformed;
|
file | diff | annotate |
| 2007-09-19 |
wenzelm |
2007-09-19 |
ml_output: proper error instead of error_msg;
|
file | diff | annotate |
| 2007-09-17 |
wenzelm |
2007-09-17 |
avoid direct access to print_mode;
|
file | diff | annotate |
| 2007-07-29 |
wenzelm |
2007-07-29 |
NAMED_CRITICAL;
|
file | diff | annotate |
| 2007-07-29 |
wenzelm |
2007-07-29 |
removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
|
file | diff | annotate |
| 2007-07-24 |
wenzelm |
2007-07-24 |
moved exception capture/release to structure Exn;
|
file | diff | annotate |
| 2007-07-23 |
wenzelm |
2007-07-23 |
marked some CRITICAL sections;
|
file | diff | annotate |
| 2007-07-23 |
wenzelm |
2007-07-23 |
marked some CRITICAL sections (for multithreading);
|
file | diff | annotate |
| 2007-07-19 |
wenzelm |
2007-07-19 |
tuned;
|
file | diff | annotate |
| 2007-07-11 |
wenzelm |
2007-07-11 |
added escape_malformed (failsafe);
|
file | diff | annotate |
| 2007-07-09 |
wenzelm |
2007-07-09 |
type output = string indicates raw system output;
|
file | diff | annotate |
| 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;
|
file | diff | annotate |
| 2007-04-30 |
wenzelm |
2007-04-30 |
explicit treatment of legacy_features;
|
file | diff | annotate |
| 2007-04-15 |
wenzelm |
2007-04-15 |
removed unused Output.panic hook -- internal to PG wrapper;
|
file | diff | annotate |
| 2007-04-04 |
wenzelm |
2007-04-04 |
cleaned-up Output functions;
removed unused info channel;
moved print_mode to ROOT.ML (generic non-sense);
|
file | diff | annotate |
| 2007-03-19 |
haftmann |
2007-03-19 |
dropped overwrite_warn
|
file | diff | annotate |
| 2007-01-31 |
haftmann |
2007-01-31 |
dropped Output.update_warn
|
file | diff | annotate |
| 2007-01-20 |
wenzelm |
2007-01-20 |
Output.debug: non-strict;
renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
|
file | diff | annotate |
| 2006-11-13 |
haftmann |
2006-11-13 |
combinator for overwriting changes with warning
|
file | diff | annotate |
| 2006-11-10 |
wenzelm |
2006-11-10 |
tuned names of start_timing,/end_timing/check_timer;
|
file | diff | annotate |
| 2006-10-09 |
wenzelm |
2006-10-09 |
moved Context.ml_output to Output.ml_output;
|
file | diff | annotate |
| 2006-09-21 |
wenzelm |
2006-09-21 |
member (op =);
|
file | diff | annotate |
| 2006-03-14 |
wenzelm |
2006-03-14 |
Output.add_mode: keyword component;
|
file | diff | annotate |
| 2006-01-19 |
wenzelm |
2006-01-19 |
added ML_errors;
|
file | diff | annotate |
| 2006-01-14 |
wenzelm |
2006-01-14 |
removed special ERROR handling stuff (transform_error etc.);
moved plain ERROR/error to library.ML;
added toplevel_errors, exception TOPLEVEL_ERROR;
error_msg, panic, info, debug no longer pervasive;
|
file | diff | annotate |
| 2005-09-21 |
haftmann |
2005-09-21 |
added update_warn
|
file | diff | annotate |
| 2005-09-20 |
haftmann |
2005-09-20 |
introduced AList module in favor of assoc etc.
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
TableFun/Symtab: curried lookup and update;
|
file | diff | annotate |
| 2005-09-01 |
wenzelm |
2005-09-01 |
curried_lookup/update;
|
file | diff | annotate |
| 2005-07-06 |
wenzelm |
2005-07-06 |
added time_accumulator and accumulated_time supercede
low-level time_info operations;
|
file | diff | annotate |
| 2005-07-04 |
wenzelm |
2005-07-04 |
added transform_exceptions: bool ref;
|
file | diff | annotate |
| 2005-06-02 |
wenzelm |
2005-06-02 |
added no_warnings;
tuned;
|
file | diff | annotate |
| 2005-02-13 |
skalberg |
2005-02-13 |
Deleted Library.option type.
|
file | diff | annotate |