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

3 files changed, 36 insertions, 6 deletions

diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 6016937d0..84091f0ab 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -189,3 +189,7 @@ Pp.ppnl (Pp.(++) (Pp.str
       X.xml_nempty "ProofTree" ["of",curi] (aux pf [])
    >]
 ;;
+
+
+(* Hook registration *)
+Xmlcommand.set_print_proof_tree print_proof_tree;;
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 58d52a09a..677cd4cd5 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 =
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 68d038f04..c82b246d4 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -34,3 +34,14 @@ val print : Libnames.reference -> string option -> unit
 (*  where dest is either None (for stdout) or (Some filename) *)
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 val show : string option -> unit
+
+(* set_print_proof_tree f                                      *)
+(*  sets a callback function f to export the proof_tree to XML *)
+val set_print_proof_tree :
+    (string ->
+     Evd.evar_map ->
+     Proof_type.proof_tree ->
+     Term.constr Proof2aproof.ProofTreeHash.t ->
+     Proof_type.proof_tree Proof2aproof.ProofTreeHash.t ->
+     string Acic.CicHash.t -> Xml.token Stream.t) ->
+    unit