X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=e2e4909428dc56f39c5bbde2edba05caaf9e7a27;hb=5b32b7905bc78c11e353efd68137b8eb7b6ac73b;hp=60b2bcdf8f4dd3003150b49d68921f3daa0580cc;hpb=c3eb2df6572479850bd087b5bc9ba948297f76cf;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 60b2bcdf8..e2e490942 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -171,9 +171,7 @@ class gui () =
         (*~comments:"comments"*)
         ~copyright:"Copyright (C) 2005, the HELM team"
         ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
-        ~logo:
-          (GdkPixbuf.from_file
-            (BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png"))
+        ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
         ~name:"Matita"
         ~version:BuildTimeConf.version
         ~website:"http://helm.cs.unibo.it"
@@ -396,7 +394,7 @@ class gui () =
       let get_devel_selected () = 
         match model#easy_mselection () with
         | [[name;_]] -> MatitamakeLib.development_for_name name
-        | _ -> assert false 
+        | _ -> None
       in
       let refresh () = 
         while Glib.Main.pending () do 
@@ -519,7 +517,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
@@ -536,8 +534,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));
@@ -548,7 +548,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;
@@ -566,7 +566,10 @@ class gui () =
         (* log *)
       MatitaLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
-        (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
+        (fun exn ->
+          if Helm_registry.get_bool "matita.catch_top_level_exn" then
+            MatitaLog.error (MatitaExcPp.to_string exn)
+          else raise exn);
         (* script *)
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
@@ -604,19 +607,19 @@ class gui () =
         let script = s () in 
         let status = script#status in
         try 
-          if source_view#buffer#modified then
-            begin
-              match ask_unsaved main#toplevel with
-              | `YES -> saveScript ()
-              | `NO -> ()
-              | `CANCEL -> raise MatitaTypes.Cancel
-            end;
-          (match script_fname with
-          | None -> ()
-          | Some fname -> 
-              ask_and_save_moo_if_needed main#toplevel fname status);
           match self#chooseFile () with
           | Some f -> 
+                if source_view#buffer#modified then
+                  begin
+                    match ask_unsaved main#toplevel with
+                    | `YES -> saveScript ()
+                    | `NO -> ()
+                    | `CANCEL -> raise MatitaTypes.Cancel
+                  end;
+                (match script_fname with
+                | None -> ()
+                | Some fname -> 
+                    ask_and_save_moo_if_needed main#toplevel fname status);
                 script#reset (); 
                 script#assignFileName f;
                 source_view#source_buffer#begin_not_undoable_action ();
@@ -1055,9 +1058,7 @@ let interactive_interp_choice () choices =
   let selection = dialog#interpChoiceTreeView#selection in
   ignore (selection#connect#changed (fun _ ->
     match selection#get_selected_rows with
-    | [path] ->
-        MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
-        interp_no := Some (model#get_interp_no path)
+    | [path] -> interp_no := Some (model#get_interp_no path)
     | _ -> assert false));
   dialog#interpChoiceDialog#show ();
   GtkThread.main ();