NEWS
changeset 16718 70c94b82c556
parent 16717 710a7a7a2b65
child 16799 978dcf30c3dd
     1.1 --- a/NEWS	Wed Jul 06 10:41:51 2005 +0200
     1.2 +++ b/NEWS	Wed Jul 06 20:00:20 2005 +0200
     1.3 @@ -406,15 +406,15 @@
     1.4  time.  For the default print mode, both Output.output and Output.raw
     1.5  have no effect.
     1.6  
     1.7 -* Pure: print_tac now outputs the goal through the trace channel.
     1.8 -
     1.9 -* Isar debugging: new reference Toplevel.debug (default false).  Set
    1.10 -to make printing of exceptions THM, TERM, TYPE and THEORY more
    1.11 -verbose.
    1.12 -
    1.13 -* Isar profiling: new reference Toplevel.profiling (default 0).  For
    1.14 -Poly/ML, set to 1 to profile time, 2 to profile space (which increases
    1.15 -the runtime).
    1.16 +* Pure: Output.time_accumulator NAME creates an operator ('a -> 'b) ->
    1.17 +'a -> 'b to measure runtime and count invocations; the cumulative
    1.18 +results are displayed at the end of a batch session.
    1.19 +
    1.20 +* Isar toplevel: improved diagnostics, mostly for Poly/ML only.
    1.21 +Reference Toplevel.debug (default false) controls detailed printing
    1.22 +and tracing of low-level exceptions; Toplevel.profiling (default 0)
    1.23 +controls execution profiling -- set to 1 for time and 2 for space
    1.24 +(both increase the runtime).
    1.25  
    1.26  * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
    1.27  reasonably efficient light-weight implementation of sets as lists.
    1.28 @@ -502,6 +502,8 @@
    1.29    PureThy.thms_of: theory -> (string * thm) list
    1.30    PureThy.all_thms_of: theory -> (string * thm) list
    1.31  
    1.32 +* Pure: print_tac now outputs the goal through the trace channel.
    1.33 +
    1.34  * Provers: Simplifier and Classical Reasoner now support proof context
    1.35  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
    1.36  components are stored in the theory and patched into the