ProofEngine.proof is now an abstract data type (since we plan to have OMDoc

[helm.git] / helm / gTopLevel / invokeTactics.ml

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 31804290930e10986ab38194c8a709e3bdc9a2b6..79b489f548532023344c2498d981d92611f12921 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -111,7 +111,7 @@ module Make (C: Callbacks) : Tactics =
   struct
 
    let call_tactic tactic () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      begin
       try
@@ -123,29 +123,29 @@ module Make (C: Callbacks) : Tactics =
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals ()
        | RefreshProofException e ->
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals () ;
           C.refresh_proof ()
        | e ->
           C.output_html
            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
+          ProofEngine.set_proof savedproof ;
           ProofEngine.goal := savedgoal
      end
 
    let call_tactic_with_input tactic ?term () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      let uri,metasenv,bo,ty =
-      match !ProofEngine.proof with
+      match ProofEngine.get_proof () with
          None -> assert false
        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
      in
@@ -165,7 +165,7 @@ module Make (C: Callbacks) : Tactics =
          | Some t -> (C.term_editor ())#set_term t);
          (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
         in
-         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+         ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
          tactic expr ;
          C.refresh_goals () ;
          C.refresh_proof () ;
@@ -175,27 +175,27 @@ module Make (C: Callbacks) : Tactics =
            C.output_html
             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
              "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal ;
            C.refresh_goals ()
         | RefreshProofException e ->
            C.output_html
             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
              "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal ;
            C.refresh_goals () ;
            C.refresh_proof ()
         | e ->
            C.output_html
             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
+           ProofEngine.set_proof savedproof ;
            ProofEngine.goal := savedgoal
 
   let call_tactic_with_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
@@ -209,21 +209,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->
@@ -236,7 +236,7 @@ module Make (C: Callbacks) : Tactics =
   let call_tactic_with_goal_inputs tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      try
       match (C.sequent_viewer ())#get_selected_terms with
@@ -252,34 +252,34 @@ module Make (C: Callbacks) : Tactics =
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals ()
       | RefreshProofException e ->
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals () ;
          C.refresh_proof ()
       | e ->
          C.output_html
           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
+         ProofEngine.set_proof savedproof ;
          ProofEngine.goal := savedgoal
 
   let call_tactic_with_input_and_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
          begin
           try
            let uri,metasenv,bo,ty =
-            match !ProofEngine.proof with
+            match ProofEngine.get_proof () with
                None -> assert false
              | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
            in
@@ -294,7 +294,7 @@ module Make (C: Callbacks) : Tactics =
             let (metasenv',expr) =
              (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
             in
-             ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+             ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
              tactic ~goal_input:term ~input:expr ;
              C.refresh_goals () ;
              C.refresh_proof () ;
@@ -304,21 +304,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->
@@ -376,7 +376,7 @@ module Make (C: Callbacks) : Tactics =
   let call_tactic_with_hypothesis_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_hypotheses with
        [hypothesis] ->
@@ -390,21 +390,21 @@ module Make (C: Callbacks) : Tactics =
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals ()
            | RefreshProofException e ->
               C.output_html
                ("<h1 color=\"red\">Exception raised during the refresh of " ^
                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
               C.refresh_goals () ;
               C.refresh_proof ()
            | e ->
               C.output_html
                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
+              ProofEngine.set_proof savedproof ;
               ProofEngine.goal := savedgoal ;
          end
      | [] ->