X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FcontentPp.ml;h=3967c621668818fbb68b8e48fcd3e2bbc96e0b32;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=3bc8bb306ae6cf0896e2d662ab9c516218856751;hpb=4bcd14a9ed245ccae631697a05ff5a377c02b179;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml
index 3bc8bb306..3967c6216 100644
--- a/helm/ocaml/cic_omdoc/contentPp.ml
+++ b/helm/ocaml/cic_omdoc/contentPp.ml
@@ -130,16 +130,26 @@ and pargs args indent =
 and parg indent =
   let module Con = Content in
   function
-       Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ (string_of_int n));flush stderr
-    |  Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise");flush stderr
+      Con.Aux n ->  prerr_endline ((blanks (indent+1)) ^ n)
+    | Con.Premise prem -> prerr_endline ((blanks (indent+1)) ^ "Premise")
+    | Con.Lemma lemma -> prerr_endline ((blanks (indent+1)) ^ "Lemma")
     | Con.Term t -> 
-        prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)));
-        flush stderr
+        prerr_endline ((blanks (indent+1)) ^ (CicPp.ppterm (Deannotate.deannotate_term t)))
     | Con.ArgProof p -> pproof p (indent+1) 
-    | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!");flush stderr
+    | Con.ArgMethod s -> prerr_endline ((blanks (indent+1)) ^ "A Method !!!")
 ;;
  
-let print_proof p = pproof p 0;
+let print_proof p = pproof p 0;;
+
+let print_obj (_,_,_,obj) =
+  match obj with 
+    `Decl (_,decl) -> 
+       pcontext_element 0 (decl:> Cic.annterm Content.in_proof_context_element)
+  | `Def (_,_,def) -> 
+       pcontext_element 0 (def:> Cic.annterm Content.in_proof_context_element)
+  | `Joint _ as jo -> pcontext_element 0 jo 
+;;
+