X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=589da7dcc8e9adb6eed32d161a7b9b583ec23b33;hb=e89367d2ad0e194c547a4e84cac87b7a48b69600;hp=bf25a5493a75ba8eb0764a9d8ffb6ee32d963d3b;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index bf25a5493..589da7dcc 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -67,14 +67,14 @@ let clean_current_baseuri status =
 
 let ask_and_save_moo_if_needed parent fname status = 
   let save () =
-    let moo_fname = MatitaMisc.obj_file_of_script fname in
+    let moo_fname = MatitacleanLib.obj_file_of_script fname in
     MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
   if (MatitaScript.current ())#eos &&
      status.MatitaTypes.proof_status = MatitaTypes.No_proof
   then
     begin
       let mooname = 
-        MatitaMisc.obj_file_of_script fname
+        MatitacleanLib.obj_file_of_script fname
       in
       let rc = 
         MatitaGtkMisc.ask_confirmation
@@ -102,7 +102,7 @@ let ask_unsaved parent =
   MatitaGtkMisc.ask_confirmation 
     ~parent ~title:"Unsaved work!" 
     ~message:("Your work is <b>unsaved</b>!\n\n"^
-         "<i>Do you want to save the script before exiting?</i>")
+         "<i>Do you want to save the script before continuing?</i>")
     ()
 
 class gui () =
@@ -605,34 +605,36 @@ class gui () =
               (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
+      let abandon_script () =
+        let status = (s ())#status in
+        if source_view#buffer#modified then
+          (match ask_unsaved main#toplevel with
+          | `YES -> saveScript ()
+          | `NO -> ()
+          | `CANCEL -> raise MatitaTypes.Cancel);
+        (match script_fname with
+        | None -> ()
+        | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+      in
       let loadScript () =
         let script = s () in 
         let status = script#status in
         try 
           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 ();
-                script#loadFromFile f; 
-                source_view#source_buffer#end_not_undoable_action ();
-                console#message ("'"^f^"' loaded.\n");
-                self#_enableSaveTo f
+              abandon_script ();
+              script#reset (); 
+              script#assignFileName f;
+              source_view#source_buffer#begin_not_undoable_action ();
+              script#loadFromFile f; 
+              source_view#source_buffer#end_not_undoable_action ();
+              console#message ("'"^f^"' loaded.\n");
+              self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        abandon_script ();
         source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template (); 
@@ -882,8 +884,8 @@ class gui () =
       dialog#check_widgets ();
       dialog
 
-    method newInterpDialog () =
-      let dialog = new interpChoiceDialog () in
+    method newRecordDialog () =
+      let dialog = new recordChoiceDialog () in
       dialog#check_widgets ();
       dialog
 
@@ -1095,30 +1097,30 @@ class interpModel =
 let interactive_interp_choice () choices =
   let gui = instance () in
   assert (choices <> []);
-  let dialog = gui#newInterpDialog () in
-  let model = new interpModel dialog#interpChoiceTreeView choices in
+  let dialog = gui#newRecordDialog () in
+  let model = new interpModel dialog#recordChoiceTreeView choices in
   let interp_len = List.length (List.hd choices) in
-  dialog#interpChoiceDialog#set_title "Interpretation choice";
-  dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+  dialog#recordChoiceDialog#set_title "Interpretation choice";
+  dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
   let interp_no = ref None in
   let return _ =
-    dialog#interpChoiceDialog#destroy ();
+    dialog#recordChoiceDialog#destroy ();
     GMain.Main.quit ()
   in
   let fail _ = interp_no := None; return () in
-  ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
-  connect_button dialog#interpChoiceOkButton (fun _ ->
+  ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
+  connect_button dialog#recordChoiceOkButton (fun _ ->
     match !interp_no with None -> () | Some _ -> return ());
-  connect_button dialog#interpChoiceCancelButton fail;
-  ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+  connect_button dialog#recordChoiceCancelButton fail;
+  ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
     interp_no := Some (model#get_interp_no path);
     return ()));
-  let selection = dialog#interpChoiceTreeView#selection in
+  let selection = dialog#recordChoiceTreeView#selection in
   ignore (selection#connect#changed (fun _ ->
     match selection#get_selected_rows with
     | [path] -> interp_no := Some (model#get_interp_no path)
     | _ -> assert false));
-  dialog#interpChoiceDialog#show ();
+  dialog#recordChoiceDialog#show ();
   GtkThread.main ();
   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)