snapshot

[helm.git] / helm / matita / matitaProof.ml

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 5612043f3b2857b0b896673d753b345cdab356e9..6c73b4b14d9cf20bc057d678add9ab036ebb14c2 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -23,11 +23,11 @@
  * http://helm.cs.unibo.it/
  *)
 
-class proofStatus ~uri ~typ =
-  object
+class proofStatus ~typ ~metasenv ~uri () =
+  object (self)
     inherit MatitaTypes.subject
 
-    val mutable _proof = (uri, [ 1, [], typ ], Cic.Meta (1, []), typ)
+    val mutable _proof = (uri, (1, [], typ) :: metasenv, Cic.Meta (1, []), typ)
     val mutable _goal = Some 1
 
     method proof = _proof
@@ -41,11 +41,11 @@ class proofStatus ~uri ~typ =
       _proof <- p;
       _goal <- Some g
 
-    method to_xml =
+    method toXml =
       let (uri, metasenv, bo, ty) = _proof in
       let currentproof =
         (* TODO CSC: Wrong: [] is just plainly wrong *)
-        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv, bo, ty, [])
       in
       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
@@ -59,15 +59,38 @@ class proofStatus ~uri ~typ =
       in
       (xml, bodyxml)
 
+    method toString =
+      let (xml, bodyxml) = self#toXml in
+      let buf = Buffer.create 10240 in
+      Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+      Buffer.add_string buf "<!DOCTYPE ConstantType SYSTEM \"http://mowgli.cs.unibo.it:58081/getdtd?uri=cic.dtd\">\n";
+      Buffer.add_string buf "<ProofStatus>\n";
+      Buffer.add_string buf (Misc.strip_xml_headings (Xml.pp_to_string xml));
+      Buffer.add_string buf (Misc.strip_xml_headings(Xml.pp_to_string bodyxml));
+      Buffer.add_string buf
+        (match _goal with
+        | None -> "<CurrentGoal />"
+        | Some goal -> Printf.sprintf "<CurrentGoal>%d</CurrentGoal>" goal);
+      Buffer.add_string buf "\n</ProofStatus>";
+      Buffer.contents buf
+
   end
 
-class proof ~uri ~typ =
+let proofStatus ~typ ?(metasenv = []) ?(uri = MatitaTypes.untitled_con_uri) () =
+  new proofStatus ~typ ~metasenv ~uri ()
+
+let proofStatus_of_string s =
+  MatitaTypes.not_implemented "MatitaProof.proofStatus_of_string"
+
+class proof ~typ ?metasenv ?uri () =
   object
-    val mutable _status = new proofStatus ~uri ~typ
+    val mutable _status = proofStatus ~typ ?metasenv ?uri ()
     method status = _status
     method setStatus s = _status <- s
   end
 
+let proof = new proof
+
 class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) =
   object
     val statusBackup = status#status