X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=79b489f548532023344c2498d981d92611f12921;hb=60c7321771851b82493bb202185ee184f1e7a3d1;hp=31804290930e10986ab38194c8a709e3bdc9a2b6;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git
diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 318042909..79b489f54 100644
--- 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
("
Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- 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
("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- 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
("Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- 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
("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- 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
("Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- 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
("Exception raised during the refresh of " ^
"the sequent: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
C.output_html
("Exception raised during the refresh of " ^
"the proof: " ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals () ;
C.refresh_proof ()
| e ->
C.output_html
("" ^ Printexc.to_string e ^ "
") ;
- ProofEngine.proof := savedproof ;
+ ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
end
| [] ->