* Hbugs interface clean-up.

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

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 96f306cdf4c8f0b97ce036d17a6d9a2873fee2a2..31804290930e10986ab38194c8a709e3bdc9a2b6 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -65,7 +65,49 @@ module type Callbacks =
   end
 ;;
 
-module Make(C:Callbacks) =
+module type Tactics =
+  sig
+   val intros : unit -> unit
+   val exact : ?term:string -> unit -> unit
+   val apply : ?term:string -> unit -> unit
+   val elimintrossimpl : ?term:string -> unit -> unit
+   val elimtype : ?term:string -> unit -> unit
+   val whd : unit -> unit
+   val reduce : unit -> unit
+   val simpl : unit -> unit
+   val fold_whd : ?term:string -> unit -> unit
+   val fold_reduce : ?term:string -> unit -> unit
+   val fold_simpl : ?term:string -> unit -> unit
+   val cut : ?term:string -> unit -> unit
+   val change : unit -> unit
+   val letin : ?term:string -> unit -> unit
+   val ring : unit -> unit
+   val clearbody : unit -> unit
+   val clear : unit -> unit
+   val fourier : unit -> unit
+   val rewritesimpl : ?term:string -> unit -> unit
+   val rewritebacksimpl : ?term:string -> unit -> unit
+   val replace : unit -> unit
+   val reflexivity : unit -> unit
+   val symmetry : unit -> unit
+   val transitivity : ?term:string -> unit -> unit
+   val exists : unit -> unit
+   val split : unit -> unit
+   val left : unit -> unit
+   val right : unit -> unit
+   val assumption : unit -> unit
+   val generalize : unit -> unit
+   val absurd : ?term:string -> unit -> unit
+   val contradiction : unit -> unit
+   val decompose : ?term:string -> unit -> unit
+   val injection : ?term:string -> unit -> unit
+   val discriminate : ?term:string -> unit -> unit
+   val whd_in_scratch : unit -> unit
+   val reduce_in_scratch : unit -> unit
+   val simpl_in_scratch : unit -> unit
+  end
+
+module Make (C: Callbacks) : Tactics =
   struct
 
    let call_tactic tactic () =
@@ -99,7 +141,7 @@ module Make(C:Callbacks) =
           ProofEngine.goal := savedgoal
      end
 
-   let call_tactic_with_input tactic () =
+   let call_tactic_with_input tactic ?term () =
     let savedproof = !ProofEngine.proof in
     let savedgoal  = !ProofEngine.goal in
      let uri,metasenv,bo,ty =
@@ -118,6 +160,9 @@ module Make(C:Callbacks) =
       in
        try
         let metasenv',expr =
+         (match term with
+         | None -> ()
+         | 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) ;
@@ -201,7 +246,7 @@ module Make(C:Callbacks) =
        | terms ->
           tactic terms ;
           C.refresh_goals () ;
-          C.refresh_proof ()
+          C.refresh_proof () ;
      with
         RefreshSequentException e ->
          C.output_html
@@ -286,8 +331,6 @@ module Make(C:Callbacks) =
   let call_tactic_with_goal_input_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
-    let savedgoal  = !ProofEngine.goal in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
        [term] ->
@@ -314,8 +357,6 @@ module Make(C:Callbacks) =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
-    let savedproof = !ProofEngine.proof in
-    let savedgoal  = !ProofEngine.goal in
      match scratch_window#sequent_viewer#get_selected_terms with
         [] ->
          C.output_html