X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.mli;h=d527e4fafa28956d83ed5745384d354ffa2a7b05;hb=2da9c5cef39f1512fc604adb30e9b0ecae4b2881;hp=df911a02f311f0ce0e5dd33f36233ec4f43b8d3a;hpb=7fe29ab0adae7bbd2589630b1c5363daf62100c9;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index df911a02f..d527e4faf 100644
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -38,29 +38,30 @@ exception RefreshProofException of exn
 
 module type Callbacks =
   sig
+    (* input widgets *)
     val sequent_viewer : unit -> TermViewer.sequent_viewer
     val term_editor : unit -> TermEditor.term_editor
-    val get_current_scratch_infos :
+    val scratch_window :
      unit ->
-      (Cic.term *
-       (Cic.id, Cic.term) Hashtbl.t *
-       (Cic.id, Cic.id option) Hashtbl.t *
-       (string, Cic.hypothesis) Hashtbl.t
-      ) option
-    val set_current_scratch_infos :
-     (Cic.term *
-      (Cic.id, Cic.term) Hashtbl.t *
-      (Cic.id, Cic.id option) Hashtbl.t *
-      (string, Cic.hypothesis) Hashtbl.t
-     ) option -> unit
+      < sequent_viewer: TermViewer.sequent_viewer ;
+        show: unit -> unit ;
+        term: Cic.term ;
+        set_term : Cic.term -> unit ;
+        metasenv: Cic.metasenv ;
+        set_metasenv : Cic.metasenv -> unit ;
+        context: Cic.context ;
+        set_context : Cic.context -> unit >
+    (* output messages *)
+    val output_html : string -> unit
+    (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
+    (* callbacks for user-tactics interaction *)
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback :
       Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
-    val output_html : string -> unit
   end
 
 module Make (C : Callbacks) :
@@ -98,16 +99,7 @@ module Make (C : Callbacks) :
    val absurd : unit -> unit
    val contradiction : unit -> unit
    val decompose : unit -> unit
-   val whd_in_scratch :
-     < mmlwidget : GMathViewAux.multi_selection_math_view;
-       show : unit -> 'a; .. > ->
-     unit -> unit
-   val reduce_in_scratch :
-     < mmlwidget : GMathViewAux.multi_selection_math_view;
-       show : unit -> 'a; .. > ->
-     unit -> unit
-   val simpl_in_scratch :
-     < mmlwidget : GMathViewAux.multi_selection_math_view;
-       show : unit -> 'a; .. > ->
-     unit -> unit
+   val whd_in_scratch : unit -> unit
+   val reduce_in_scratch : unit -> unit
+   val simpl_in_scratch : unit -> unit
  end