# HG changeset patch
# User wenzelm
# Date 1120672820 -7200
# Node ID 70c94b82c556826b96200abace1ad09840abfcbc
# Parent  710a7a7a2b658c8da16825a79e7afb2658daf74c
* Pure: Output.time_accumulator;
* Isar toplevel: improved diagnostics;

diff -r 710a7a7a2b65 -r 70c94b82c556 NEWS
--- a/NEWS	Wed Jul 06 10:41:51 2005 +0200
+++ b/NEWS	Wed Jul 06 20:00:20 2005 +0200
@@ -406,15 +406,15 @@
 time.  For the default print mode, both Output.output and Output.raw
 have no effect.
 
-* Pure: print_tac now outputs the goal through the trace channel.
-
-* Isar debugging: new reference Toplevel.debug (default false).  Set
-to make printing of exceptions THM, TERM, TYPE and THEORY more
-verbose.
-
-* Isar profiling: new reference Toplevel.profiling (default 0).  For
-Poly/ML, set to 1 to profile time, 2 to profile space (which increases
-the runtime).
+* Pure: Output.time_accumulator NAME creates an operator ('a -> 'b) ->
+'a -> 'b to measure runtime and count invocations; the cumulative
+results are displayed at the end of a batch session.
+
+* Isar toplevel: improved diagnostics, mostly for Poly/ML only.
+Reference Toplevel.debug (default false) controls detailed printing
+and tracing of low-level exceptions; Toplevel.profiling (default 0)
+controls execution profiling -- set to 1 for time and 2 for space
+(both increase the runtime).
 
 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
 reasonably efficient light-weight implementation of sets as lists.
@@ -502,6 +502,8 @@
   PureThy.thms_of: theory -> (string * thm) list
   PureThy.all_thms_of: theory -> (string * thm) list
 
+* Pure: print_tac now outputs the goal through the trace channel.
+
 * Provers: Simplifier and Classical Reasoner now support proof context
 dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
 components are stored in the theory and patched into the