New policy for the disambiguation passes.

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index cf141722992e3d49ccba720beba267d0396867d7..153d474abe09b6a5e22baff307ebcaac3cc0283a 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -80,7 +80,7 @@ let ask_and_save_moo_if_needed parent fname status =
         ~title:"A .moo can be generated"
         ~message:(Printf.sprintf 
           "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          mooname fname)
+          (Filename.basename mooname) (Filename.basename fname))
         ~parent ()
       in
       let b = 
@@ -129,11 +129,6 @@ class gui () =
       ~default:BuildTimeConf.default_font_size "matita.font_size"
   in
   let source_buffer = source_view#source_buffer in
-(*   let _ =
-    source_view#event#connect#selection_clear (fun _ ->
-      prerr_endline "source_view: selection clear";
-      false)
-  in *)
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
@@ -176,8 +171,9 @@ class gui () =
         (*~comments:"comments"*)
         ~copyright:"Copyright (C) 2005, the HELM team"
         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
-        (*?logo:GdkPixbuf.pixbuf*)
-        (*?logo_icon_name:string*)
+        ~logo:
+          (GdkPixbuf.from_file
+            (BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png"))
         ~name:"Matita"
         ~version:BuildTimeConf.version
         ~website:"http://helm.cs.unibo.it"
@@ -523,7 +519,7 @@ class gui () =
         (* toolbar *)
       let module A = GrafiteAst in
       let hole = CicNotationPt.UserInput in
-      let loc = Disambiguate.dummy_floc in
+      let loc = DisambiguateTypes.dummy_floc in
       let tac ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           (MatitaScript.instance ())#advance
@@ -540,8 +536,10 @@ class gui () =
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
-      connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
-      connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
+      connect_button tbar#elimButton (tac_w_term
+        (A.Elim (loc, hole, None, None, [])));
+      connect_button tbar#elimTypeButton (tac_w_term
+        (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));
       connect_button tbar#leftButton (tac (A.Left loc));
       connect_button tbar#rightButton (tac (A.Right loc));
@@ -552,7 +550,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None)));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;