From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 20 Feb 2003 17:24:43 +0000 (+0000)
Subject: - added HBugs notification after tactic application
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5ff3bf7bda01b5194e502aef5e9e47a49ecf1ad;p=helm.git

- added HBugs notification after tactic application
- bugfix: removed some useless status save
- defined module type "Tactics", module type returned by Make functor
---

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 96f306cdf..775d6a468 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -62,10 +62,54 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback :
       Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    (* invoked when the proof assistant's status has changed to notify Hbugs *)
+    val notify_hbugs : unit -> unit
   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 () =
@@ -75,7 +119,8 @@ module Make(C:Callbacks) =
       try
        tactic () ;
        C.refresh_goals () ;
-       C.refresh_proof ()
+       C.refresh_proof () ;
+       C.notify_hbugs ()
       with
          RefreshSequentException e ->
           C.output_html
@@ -99,7 +144,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,13 +163,17 @@ 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) ;
          tactic expr ;
          C.refresh_goals () ;
          C.refresh_proof () ;
-         (C.term_editor ())#reset
+         (C.term_editor ())#reset ;
+         C.notify_hbugs ()
        with
           RefreshSequentException e ->
            C.output_html
@@ -158,7 +207,8 @@ module Make(C:Callbacks) =
           try
            tactic term ;
            C.refresh_goals () ;
-           C.refresh_proof ()
+           C.refresh_proof () ;
+           C.notify_hbugs ()
           with
              RefreshSequentException e ->
               C.output_html
@@ -201,7 +251,8 @@ module Make(C:Callbacks) =
        | terms ->
           tactic terms ;
           C.refresh_goals () ;
-          C.refresh_proof ()
+          C.refresh_proof () ;
+          C.notify_hbugs ()
      with
         RefreshSequentException e ->
          C.output_html
@@ -253,7 +304,8 @@ module Make(C:Callbacks) =
              tactic ~goal_input:term ~input:expr ;
              C.refresh_goals () ;
              C.refresh_proof () ;
-             (C.term_editor ())#reset
+             (C.term_editor ())#reset ;
+             C.notify_hbugs ()
           with
              RefreshSequentException e ->
               C.output_html
@@ -286,8 +338,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 +364,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
@@ -343,7 +391,8 @@ module Make(C:Callbacks) =
           try
            tactic hypothesis ;
            C.refresh_goals () ;
-           C.refresh_proof ()
+           C.refresh_proof () ;
+           C.notify_hbugs ()
           with
              RefreshSequentException e ->
               C.output_html
diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 313991ced..11b8ecf72 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -62,46 +62,50 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback :
       Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val notify_hbugs : unit -> unit
   end
 
-module Make (C : Callbacks) :
+module type Tactics =
  sig
    val intros : unit -> unit
-   val exact : unit -> unit
-   val apply : unit -> unit
-   val elimintrossimpl : unit -> unit
-   val elimtype : 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 : unit -> unit
-   val fold_reduce : unit -> unit
-   val fold_simpl : unit -> unit
-   val cut : 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 : 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 : unit -> unit
-   val rewritebacksimpl : 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 : 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 : unit -> unit
+   val absurd : ?term:string -> unit -> unit
    val contradiction : unit -> unit
-   val decompose : unit -> unit
-   val injection : unit -> unit
-   val discriminate : 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
+