better dependencies among modules and symlinking of several matitatools to a single...

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index bf25a5493a75ba8eb0764a9d8ffb6ee32d963d3b..d4157677feabd3573bae00edf5c4d84d52795c3d 100644 (file)
--- 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
@@ -882,8 +882,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 +1095,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)