X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=13dc83f1d02dbba6531d18db4e70d5f0fdbc3321;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=2b0e58d214328d4a7e7c18b5600658a9ac4e283f;hpb=feb3c287997f7d35747c12e0db62e6194f5587a3;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 2b0e58d21..13dc83f1d 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -53,8 +53,6 @@ module type Callbacks =
         set_metasenv : Cic.metasenv -> unit ;
         context: Cic.context ;
         set_context : Cic.context -> unit >
-    (* output messages *)
-    val output_html : Ui_logger.html_msg -> unit
     (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
@@ -63,6 +61,8 @@ module type Callbacks =
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+    val mqi_handle : MQIConn.handle
+    val dbd:Mysql.dbd
   end
 ;;
 
@@ -106,13 +106,14 @@ module type Tactics =
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
+   val auto : unit -> unit 
   end
 
 module Make (C: Callbacks) : Tactics =
   struct
 
    let print_uncaught_exception e =
-     C.output_html (`Error (`T (sprintf "Uncaught exception: %s"
+     HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
       (Printexc.to_string e))))
 
    let handle_refresh_exception f savedproof savedgoal =
@@ -120,14 +121,14 @@ module Make (C: Callbacks) : Tactics =
        f ()
      with
      | RefreshSequentException e ->
-        C.output_html (`Error (`T
+        HelmLogger.log (`Error (`T
           (sprintf "Exception raised during the refresh of the sequent: %s"
             (Printexc.to_string e))));
         ProofEngine.set_proof savedproof ;
         ProofEngine.goal := savedgoal ;
         C.refresh_goals ()
      | RefreshProofException e ->
-        C.output_html (`Error (`T
+        HelmLogger.log (`Error (`T
           (sprintf "Exception raised during the refresh of the proof: %s"
             (Printexc.to_string e))));
         ProofEngine.set_proof savedproof ;
@@ -168,7 +169,7 @@ module Make (C: Callbacks) : Tactics =
       in
        handle_refresh_exception
         (fun () ->
-          let metasenv',expr =
+          let metasenv',expr,ugraph = (*TASSI:  FIX THIS*)
            (match term with
            | None -> ()
            | Some t -> (C.term_editor ())#set_term t);
@@ -194,8 +195,8 @@ module Make (C: Callbacks) : Tactics =
             C.refresh_goals () ;
             C.refresh_proof ())
           savedproof savedgoal
-     | [] -> C.output_html (`Error (`T "No term selected"))
-     | _ -> C.output_html (`Error (`T "Too many terms selected"))
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs tactic () =
    let module L = LogicalOperations in
@@ -205,7 +206,7 @@ module Make (C: Callbacks) : Tactics =
      handle_refresh_exception
       (fun () ->
         match (C.sequent_viewer ())#get_selected_terms with
-         | [] -> C.output_html (`Error (`T "No term selected"))
+         | [] -> HelmLogger.log (`Error (`T "No term selected"))
          | terms ->
             tactic terms ;
             C.refresh_goals () ;
@@ -234,7 +235,7 @@ module Make (C: Callbacks) : Tactics =
                     List.find (function (m,_,_) -> m=metano) metasenv
                    in
                     canonical_context in
-              let (metasenv',expr) =
+              let (metasenv',expr,ugraph) =(* FIX THIS AND *)
                (C.term_editor ())#get_metasenv_and_term
                 canonical_context metasenv
               in
@@ -244,8 +245,8 @@ module Make (C: Callbacks) : Tactics =
                C.refresh_proof () ;
                (C.term_editor ())#reset)
           savedproof savedgoal
-     | [] -> C.output_html (`Error (`T "No term selected"))
-     | _ -> C.output_html (`Error (`T "Too many terms selected"))
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_input_in_scratch tactic () =
    let module L = LogicalOperations in
@@ -263,15 +264,15 @@ module Make (C: Callbacks) : Tactics =
           with
            e -> print_uncaught_exception e
          end
-     | [] -> C.output_html (`Error (`T "No term selected"))
-     | _ -> C.output_html (`Error (`T "Too many terms selected"))
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
-      | [] -> C.output_html (`Error (`T "No term selected"))
+      | [] -> HelmLogger.log (`Error (`T "No term selected"))
       | terms ->
          try
           let expr = tactic terms scratch_window#term in
@@ -295,8 +296,9 @@ module Make (C: Callbacks) : Tactics =
              C.refresh_goals () ;
              C.refresh_proof ())
            savedproof savedgoal
-     | [] -> C.output_html (`Error (`T "No hypothesis selected"))
-     | _ -> C.output_html (`Error (`T "Too many hypotheses selected"))
+     | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
+
 
 
   let intros =
@@ -304,6 +306,7 @@ module Make (C: Callbacks) : Tactics =
     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
   let exact = call_tactic_with_input ProofEngine.exact
   let apply = call_tactic_with_input ProofEngine.apply
+  let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
   let elimtype = call_tactic_with_input ProofEngine.elim_type
   let whd = call_tactic_with_goal_inputs ProofEngine.whd