ProofTree2Xml is no longer directly used by Xmlcommand.

On the contrary, it registers itself using the hook provided by
Xmlcommand. The obtained design is more modular.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5563 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 6 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 58d52a09a7..677cd4cd5b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -19,8 +19,22 @@
 
 (* CONFIGURATION PARAMETERS *)
 
-(*CSC: was false*)
-let verbose = ref true;; (* always set to true during a "Print XML All" *)
+let verbose = ref false;; (* always set to true during a "Print XML All" *)
+
+(* HOOKS *)
+let print_proof_tree, set_print_proof_tree =
+ let print_proof_tree = ref (fun _ _ _ _ _ _ -> None) in
+  (fun () -> !print_proof_tree),
+   (fun f ->
+     print_proof_tree :=
+     fun
+      curi sigma0 pf proof_tree_to_constr proof_tree_to_flattened_proof_tree
+      constr_to_ids
+     ->
+      Some
+       (f curi sigma0 pf proof_tree_to_constr
+        proof_tree_to_flattened_proof_tree constr_to_ids))
+;;
 
 (* UTILITY FUNCTIONS *)
 
@@ -219,14 +233,15 @@ let print_object uri obj sigma proof_tree_infos filename =
      None -> ()
    | Some (sigma0,proof_tree,proof_tree_to_constr,
            proof_tree_to_flattened_proof_tree) ->
-(*CSC: bug in V8
       let xmlprooftree =
-       ProofTree2Xml.print_proof_tree
+       print_proof_tree ()
         uri sigma0 proof_tree proof_tree_to_constr
         proof_tree_to_flattened_proof_tree constr_to_ids
       in
-       pp xmlprooftree (prooftree_filename_of_filename filename)
-*) ()
+       match xmlprooftree with
+          None -> ()
+        | Some xmlprooftree ->
+           pp xmlprooftree (prooftree_filename_of_filename filename)
 ;;
 
 let string_list_of_named_context_list =