X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=1d433f848a2f988dd42cde1c313c5048abbc15ad;hb=ecd0ab19b82f611974bd76f3c740c842f566009d;hp=1e2b548267d9f95f31da8221b3c97c81fca90d0b;hpb=a956992315e3a723c69dff5edc361ea3db75cd54;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 1e2b54826..1d433f848 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -42,7 +42,7 @@ end
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
-    val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+    val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
     val message_tag = buffer#create_tag []
     val debug_tag   = buffer#create_tag [ `FOREGROUND "#888888" ]
     method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
@@ -58,12 +58,60 @@ class console ~(buffer: GText.buffer) () =
       | `Message -> self#message (s ^ "\n")
       | `Warning -> self#warning (s ^ "\n")
   end
+        
+let clean_current_baseuri status = 
+    try  
+      let baseuri = MatitaTypes.get_string_option status "baseuri" in
+      MatitacleanLib.clean_baseuris [baseuri]
+    with MatitaTypes.Option_error _ -> ()
+
+let ask_and_save_moo_if_needed parent fname status = 
+  let save () =
+    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+  if (MatitaScript.instance ())#eos &&
+     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+  then
+    begin
+      let mooname = 
+        MatitaMisc.obj_file_of_script fname
+      in
+      let rc = 
+        MatitaGtkMisc.ask_confirmation
+        ~title:"A .moo can be generated"
+        ~message:(Printf.sprintf 
+          "%s can be generated for %s.\n<i>Should I generate it?</i>"
+          mooname fname)
+        ~parent ()
+      in
+      let b = 
+        match rc with 
+        | `YES -> true 
+        | `NO -> false 
+        | `CANCEL -> raise MatitaTypes.Cancel 
+      in
+      if b then
+        save ()
+      else
+        clean_current_baseuri status
+    end
+  else
+    clean_current_baseuri status 
+    
+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>")
+    ()
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)
   let main = new mainWin () in
   let about = new aboutWin () in
   let fileSel = new fileSelectionWin () in
+  let findRepl = new findReplWin () in
+  let develList = new develListWin () in
+  let newDevel = new newDevelopmentWin () in
   let keyBindingBoxes = (* event boxes which should receive global key events *)
     [ main#mainWinEventBox ]
   in
@@ -85,14 +133,16 @@ class gui () =
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
+    val mutable _only_directory = false
     val mutable script_fname = None
     val mutable font_size = default_font_size
+    val mutable next_devel_must_contain = None
    
     initializer
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
         (let c w = (w :> <check_widgets: unit -> unit>) in
-         [ c about; c fileSel; c main ]);
+        [ c about; c fileSel; c main; c findRepl]);
         (* key bindings *)
       List.iter (* global key bindings *)
         (fun (key, callback) -> self#addKeyBinding key callback)
@@ -111,6 +161,137 @@ class gui () =
         about#aboutWin#misc#hide ());
       about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
         ~templ:BuildTimeConf.version about#aboutLabel#label);
+        (* findRepl win *)
+      let show_find_Repl () = 
+        findRepl#toplevel#misc#show ();
+        findRepl#toplevel#misc#grab_focus ()
+      in
+      let hide_find_Repl () = findRepl#toplevel#misc#hide () in
+      let find_forward _ = 
+          let highlight start end_ =
+            source_buffer#move_mark `INSERT ~where:start;
+            source_buffer#move_mark `SEL_BOUND ~where:end_
+          in
+          let text = findRepl#findEntry#text in
+          let iter = source_buffer#get_iter `SEL_BOUND in
+          match iter#forward_search text with
+          | None -> 
+              (match source_buffer#start_iter#forward_search text with
+              | None -> ()
+              | Some (start,end_) -> highlight start end_)
+          | Some (start,end_) -> highlight start end_ 
+      in
+      let replace _ =
+        let text = findRepl#replaceEntry#text in
+        let ins = source_buffer#get_iter `INSERT in
+        let sel = source_buffer#get_iter `SEL_BOUND in
+        if ins#compare sel < 0 then 
+          begin
+            ignore(source_buffer#delete_selection ());
+            source_buffer#insert text
+          end
+      in
+      connect_button findRepl#findButton find_forward;
+      connect_button findRepl#findReplButton replace;
+      connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
+      ignore(findRepl#toplevel#event#connect#delete 
+        ~callback:(fun _ -> hide_find_Repl ();true));
+      ignore(self#main#findReplMenuItem#connect#activate
+        ~callback:show_find_Repl);
+      ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+        (* developments win *)
+      let model = 
+        new MatitaGtkMisc.multiStringListModel 
+          ~cols:2 develList#developmentsTreeview
+      in
+      let refresh_devels_win () =
+        model#list_store#clear ();
+        List.iter 
+          (fun (name, root) -> model#easy_mappend [name;root]) 
+          (MatitamakeLib.list_known_developments ())
+      in
+      let get_devel_selected () = 
+        match model#easy_mselection () with
+        | [[name;_]] -> MatitamakeLib.development_for_name name
+        | _ -> assert false 
+      in
+      connect_button develList#newButton
+        (fun () -> 
+          next_devel_must_contain <- None;
+          newDevel#toplevel#misc#show());
+      connect_button develList#deleteButton
+        (fun () -> 
+          (match get_devel_selected () with
+          | None -> ()
+          | Some d -> MatitamakeLib.destroy_development d);
+          refresh_devels_win ());
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
+      connect_button develList#buildButton 
+        (fun () -> 
+          match get_devel_selected () with
+          | None -> ()
+          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+      connect_button develList#cleanButton 
+        (fun () -> 
+          match get_devel_selected () with
+          | None -> ()
+          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+      connect_button develList#closeButton 
+        (fun () -> develList#toplevel#misc#hide());
+      ignore(develList#toplevel#event#connect#delete 
+        (fun _ -> develList#toplevel#misc#hide();true));
+      let selected_devel = ref None in
+      connect_menu_item self#main#developmentsMenuItem
+        (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
+      
+        (* add development win *)
+      let check_if_root_contains root =
+        match next_devel_must_contain with
+        | None -> true
+        | Some path -> 
+            let is_prefix_of d1 d2 =
+              let len1 = String.length d1 in
+              let len2 = String.length d2 in
+              if len2 < len1 then 
+                false
+              else
+                let pref = String.sub d2 0 len1 in
+                pref = d1
+            in
+            is_prefix_of root path
+      in
+      connect_button newDevel#addButton 
+       (fun () -> 
+          let name = newDevel#nameEntry#text in
+          let root = newDevel#rootEntry#text in
+          if check_if_root_contains root then
+            begin
+              ignore (MatitamakeLib.initialize_development name root);
+              refresh_devels_win ();
+              newDevel#nameEntry#set_text "";
+              newDevel#rootEntry#set_text "";
+              newDevel#toplevel#misc#hide()
+            end
+          else
+            MatitaLog.error ("The selected root does not contain " ^ 
+              match next_devel_must_contain with 
+              | Some x -> x 
+              | _ -> assert false));
+      connect_button newDevel#chooseRootButton 
+       (fun () ->
+         let path = self#chooseDir () in
+         match path with
+         | Some path -> newDevel#rootEntry#set_text path
+         | None -> ());
+      connect_button newDevel#cancelButton 
+       (fun () -> newDevel#toplevel#misc#hide ());
+      ignore(newDevel#toplevel#event#connect#delete 
+        (fun _ -> newDevel#toplevel#misc#hide();true));
+      
         (* file selection win *)
       ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
       ignore (fileSel#fileSelectionWin#connect#response (fun event ->
@@ -123,9 +304,17 @@ class gui () =
         | `OK ->
             let fname = fileSel#fileSelectionWin#filename in
             if Sys.file_exists fname then
-              (if is_regular fname then return (Some fname))
+              begin
+                if is_regular fname && not(_only_directory) then 
+                  return (Some fname) 
+                else if _only_directory && is_dir fname then 
+                  return (Some fname)
+              end
             else
-              (if _ok_not_exists then return (Some fname))
+              begin
+                if _ok_not_exists then 
+                  return (Some fname)
+              end
         | `CANCEL -> return None
         | `HELP -> ()
         | `DELETE_EVENT -> return None));
@@ -134,30 +323,31 @@ class gui () =
       main#helpMenu#set_right_justified true;
         (* console *)
       let adj = main#logScrolledWin#vadjustment in
-      ignore (adj#connect#changed
+        ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
         (* toolbar *)
-      let module A = TacticAst in
-      let hole = CicAst.UserInput in
-      let loc = CicAst.dummy_floc in
+      let module A = GrafiteAst in
+      let hole = CicNotationPt.UserInput in
+      let loc = Disambiguate.dummy_floc in
       let tac ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           (MatitaScript.instance ())#advance
-            ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+            ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+            ()
       in
       let tac_w_term ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n" ^ TacticAstPp.pp_tactic ast)
+            ("\n" ^ GrafiteAstPp.pp_tactic ast)
       in
       let tbar = self#main in
       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)));
-      connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (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#splitButton (tac (A.Split loc));
       connect_button tbar#leftButton (tac (A.Left loc));
       connect_button tbar#rightButton (tac (A.Right loc));
@@ -183,14 +373,10 @@ class gui () =
           | false -> self#main#toplevel#unfullscreen ())
         ~check:self#main#fullscreenMenuItem;
       self#main#fullscreenMenuItem#set_active false;
-        (* quit *)
-      self#setQuitCallback (fun () -> exit 0);
         (* log *)
       MatitaLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
-        (fun exn ->
-           MatitaLog.error
-             (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+        (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
         (* script *)
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
@@ -206,17 +392,6 @@ class gui () =
         script_fname <- None;
         self#main#saveMenuItem#misc#set_sensitive false
       in
-      let loadScript () =
-        let script = s () in
-        match self#chooseFile () with
-        | Some f -> 
-              script#reset (); 
-              script#assignFileName f;
-              script#loadFromFile (); 
-              console#message ("'"^f^"' loaded.\n");
-              self#_enableSaveTo f
-        | None -> ()
-      in
       let saveAsScript () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
@@ -235,22 +410,102 @@ class gui () =
               (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
-      let newScript () = (s ())#reset (); disableSave () in
+      let loadScript () =
+        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 -> 
+                script#reset (); 
+                script#assignFileName f;
+                script#loadFromFile (); 
+                console#message ("'"^f^"' loaded.\n");
+                self#_enableSaveTo f
+          | None -> ()
+        with MatitaTypes.Cancel -> ()
+      in
+      let newScript () = 
+        (s ())#reset (); 
+        (s ())#template (); 
+        disableSave ();
+        script_fname <- None
+      in
       let cursor () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
       in
+      let lock_world _ =
+        main#buttonsToolbar#misc#set_sensitive false;
+        source_view#set_editable false
+      in
+      let unlock_world _ =
+        main#buttonsToolbar#misc#set_sensitive true;
+        source_view#set_editable true
+      in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
+      let locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+      in
+      let advance = locker advance in
+      let retract = locker retract in
+      let top = locker top in
+      let bottom = locker bottom in
+      let jump = locker jump in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;
         connect_key self#sourceView#event
           ~modifiers:[`CONTROL] ~stop:true sym f
       in
+        (* quit *)
+      self#setQuitCallback (fun () -> 
+        let status = (MatitaScript.instance ())#status in
+        if source_view#buffer#modified then
+          begin
+            let rc = ask_unsaved main#toplevel in 
+            try
+              match rc with
+              | `YES -> saveScript ();
+                        if not source_view#buffer#modified then
+                          begin
+                            (match script_fname with
+                            | None -> ()
+                            | Some fname -> 
+                               ask_and_save_moo_if_needed 
+                                 main#toplevel fname status);
+                          GMain.Main.quit ()
+                          end
+              | `NO -> GMain.Main.quit ()
+              | `CANCEL -> raise MatitaTypes.Cancel
+            with MatitaTypes.Cancel -> ()
+          end 
+        else 
+          begin  
+            (match script_fname with
+            | None -> clean_current_baseuri status; GMain.Main.quit ()
+            | Some fname ->
+                try
+                  ask_and_save_moo_if_needed main#toplevel fname status;
+                  GMain.Main.quit ()
+                with MatitaTypes.Cancel -> ())
+          end);
       connect_button self#main#scriptAdvanceButton advance;
       connect_button self#main#scriptRetractButton retract;
       connect_button self#main#scriptTopButton top;
@@ -291,13 +546,23 @@ class gui () =
       let main_h = height * 80 / 100 in
       let script_w = main_w * 6 / 10 in
       self#main#toplevel#resize ~width:main_w ~height:main_h;
-      self#main#hpaneScriptSequent#set_position script_w  
+      self#main#hpaneScriptSequent#set_position script_w;
+        (* source_view *)
+      ignore(source_view#connect#after#paste_clipboard 
+        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
     
     method loadScript file =       
       let script = MatitaScript.instance () in
       script#reset (); 
       script#assignFileName file;
-      script#loadFromFile (); 
+      if not (Sys.file_exists file) then
+        begin
+          let oc = open_out file in
+          let template = MatitaMisc.input_file BuildTimeConf.script_template in 
+          output_string oc template;
+          close_out oc
+        end;
+      script#loadFromFile ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
       
@@ -317,7 +582,10 @@ class gui () =
     method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
     method about = about
     method fileSel = fileSel
+    method findRepl = findRepl
     method main = main
+    method develList = develList
+    method newDevel = newDevel
 
     method newBrowserWin () =
       object (self)
@@ -356,15 +624,29 @@ class gui () =
         keyBindingBoxes
 
     method setQuitCallback callback =
-      ignore (main#toplevel#connect#destroy callback);
       ignore (main#quitMenuItem#connect#activate callback);
+      ignore (main#toplevel#event#connect#delete 
+        (fun _ -> callback ();true));
       self#addKeyBinding GdkKeysyms._q callback
 
     method chooseFile ?(ok_not_exists = false) () =
       _ok_not_exists <- ok_not_exists;
+      _only_directory <- false;
+      fileSel#fileSelectionWin#show ();
+      GtkThread.main ();
+      chosen_file
+
+    method private chooseDir ?(ok_not_exists = false) () =
+      _ok_not_exists <- ok_not_exists;
+      _only_directory <- true;
       fileSel#fileSelectionWin#show ();
       GtkThread.main ();
+      (* we should check that this is a directory *)
       chosen_file
+  
+    method createDevelopment ~containing =
+      next_devel_must_contain <- containing;
+      newDevel#toplevel#misc#show()
 
     method askText ?(title = "") ?(msg = "") () =
       let dialog = new textDialog () in