- added and exposed get_current_status_as_xml

- removed apply_tactic and can_apply_tactic

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index afa63689bf64daceda2e4dc14f2c3e9e878121a9..491fe5224f2098cf1fc87765a52c62e5e99db4f4 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -31,34 +31,43 @@ open ProofEngineTypes
 let proof = ref (None : proof option)
 let goal = ref (None : goal option)
 
-let apply_or_can_apply_tactic ~try_only ~tactic =
+let get_current_status_as_xml () =
+  match !proof with
+     None -> assert false
+   | Some (uri, metasenv, bo, ty) ->
+      let currentproof =
+       (*CSC: Wrong: [] is just plainly wrong *)
+       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+      in
+       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
+        Cic2acic.acic_object_of_cic_object currentproof
+       in
+        let xml, bodyxml =
+         match
+          Cic2Xml.print_object uri ~ids_to_inner_sorts
+           ~ask_dtd_to_the_getter:true acurrentproof
+         with
+            xml,Some bodyxml -> xml,bodyxml
+          | _,None -> assert false
+        in
+         (xml, bodyxml)
+;;
+
+let apply_tactic ~tactic =
  match !proof,!goal with
-    None,_
+  | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
      let (newproof, newgoals) = tactic ~status:(proof', goal') in
-      if not try_only then
-       begin
-        proof := Some newproof;
-        goal :=
-         (match newgoals, newproof with
-             goal::_, _ -> Some goal
-           | [], (_,(goal,_,_)::_,_,_) ->
-           (* the tactic left no open goal ; let's choose the first open goal *)
-(*CSC: here we could implement and use a proof-tree like notion... *)
-              Some goal
-           | _, _ -> None)
-       end
-;;
-
-let apply_tactic = apply_or_can_apply_tactic ~try_only:false;;
-
-let can_apply_tactic ~tactic =
- try
-  apply_or_can_apply_tactic ~try_only:true ~tactic ;
-  true
- with
-  Fail _ -> false
+      proof := Some newproof;
+      goal :=
+       (match newgoals, newproof with
+           goal::_, _ -> Some goal
+         | [], (_,(goal,_,_)::_,_,_) ->
+         (* the tactic left no open goal ; let's choose the first open goal *)
+         (*CSC: here we could implement and use a proof-tree like notion... *)
+            Some goal
+         | _, _ -> None)
 ;;
 
 (* metas_in_term term                                                *)
@@ -163,7 +172,6 @@ let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl
 
   (* primitive tactics *)
 
-let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
 let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
 let intros ?mk_fresh_name_callback () =
  apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ())

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index c75dc437fe00f5eba77b6b7ec70ef8bb0acc9fda..4b7db8fe6346dce46302692bad87de265fa89648 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -27,6 +27,10 @@
 val proof : ProofEngineTypes.proof option ref
 val goal : ProofEngineTypes.goal option ref
 
+  (** return a pair of "xml" (as defined in Xml module) representing the current
+  proof type and body, respectively *)
+val get_current_status_as_xml : unit -> Xml.token Stream.t * Xml.token Stream.t
+
   (* start a new goal undoing part of the proof *)
 val perforate : Cic.context -> Cic.term -> Cic.term -> unit
 
@@ -44,7 +48,6 @@ val reduce_in_scratch : Cic.term list -> Cic.term -> Cic.term
 val simpl_in_scratch : Cic.term list -> Cic.term -> Cic.term
 
   (* "primitive" tactics *)
-val can_apply : Cic.term -> bool
 val apply : Cic.term -> unit
 val intros :
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> unit