X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=1d433f848a2f988dd42cde1c313c5048abbc15ad;hb=ecd0ab19b82f611974bd76f3c740c842f566009d;hp=b54dbb777f2e57f7e898d5510f7dcf7b0232ca03;hpb=57b43a967eaf3b0747350cd775d4301a53af2820;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index b54dbb777..1d433f848 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -110,6 +110,8 @@ class gui () = 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 @@ -131,8 +133,10 @@ 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 *) @@ -195,6 +199,99 @@ class gui () = 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 -> @@ -207,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)); @@ -218,23 +323,24 @@ 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, []))); @@ -339,11 +445,29 @@ class gui () = 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; @@ -460,6 +584,8 @@ class gui () = method fileSel = fileSel method findRepl = findRepl method main = main + method develList = develList + method newDevel = newDevel method newBrowserWin () = object (self) @@ -505,9 +631,22 @@ class gui () = 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