Synchronize the profiler state with the document

This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily.  I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid.  That said, a few simple tests seem to indicate that this
works as expected.

3 files changed, 19 insertions, 4 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 24f4b2a775..608793d04f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1204,7 +1204,7 @@ It is possible to measure the time spent in invocations of primitive tactics as
 \begin{quote}
 {\tt Start Profiling}.
 \end{quote}
-Enables the profiler and resets the profile
+Enables the profiler
 
 \begin{quote}
 {\tt Stop Profiling}.
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index 0c4e0b0757..ce00c29202 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -19,7 +19,7 @@ END;;
 
 
 VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF
- [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ]
+ [ "Start" "Profiling" ] -> [ set_profiling true ]
 END
 
 VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF
diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml
index 71b96614ce..6ae07689dd 100644
--- a/ltacprof/profile_ltac.ml
+++ b/ltacprof/profile_ltac.ml
@@ -3,7 +3,8 @@ open Printer
 open Util
 
 
-let is_profiling = ref false
+(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. *)
+let is_profiling = Summary.ref false ~name:"is-profiling-ltac"
 let set_profiling b = is_profiling := b
 
 let should_display_profile_at_close = ref false
@@ -40,7 +41,21 @@ let add_entry e add_total {total; local; ncalls; max_total} =
   if add_total then e.max_total <- max e.max_total max_total
 
 type treenode = {entry : entry; children : (string, treenode) Hashtbl.t}
-let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}]
+
+(** Tobias Tebbi wrote some tricky code involving mutation.  Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *)
+let deepcopy_entry {total; local; ncalls; max_total} =
+  {total; local; ncalls; max_total}
+
+let rec deepcopy_treenode {entry; children} =
+  {entry = deepcopy_entry entry;
+   children =
+      (let children' = Hashtbl.create (Hashtbl.length children) in
+       Hashtbl.iter
+	 (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree))
+	 children;
+       children')}
+
+let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack"
 
 let on_stack = Hashtbl.create 5