X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=b294af25d45a5ed7c46a1e0dd991a317c39c82c8;hb=881672563cb65777d23c9dbe2c24de5214c82eb3;hp=d8916f7fa923e21cf11b9b25644f9628a171a360;hpb=1eba57d6ae8c7cb8adab81cf50674adaaa55eccc;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index d8916f7fa..b294af25d 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -128,15 +128,19 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri status = LibraryClean.clean_baseuris [status#baseuri] -let save_moo status = - let script = MatitaScript.current () in +let save_moo0 ~do_clean script status = let baseuri = status#baseuri in match script#bos, script#eos with | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) status - | _ -> clean_current_baseuri status + | _ -> if do_clean then clean_current_baseuri status +;; + +let save_moo status = + let script = MatitaScript.current () in + save_moo0 ~do_clean:true script status ;; let ask_unsaved parent filename = @@ -251,7 +255,7 @@ class interpErrorModel = exception UseLibrary;; let interactive_error_interp ~all_passes - (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename + (source_buffer:GSourceView3.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) if false then @@ -405,7 +409,6 @@ class gui () = let main = new mainWin () in let sequents_viewer = MatitaMathView.sequentsViewer_instance main#sequentsNotebook in - let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] @@ -415,19 +418,24 @@ class gui () = val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false + val mutable current_page = -1 initializer let s () = MatitaScript.current () in (* key bindings *) List.iter (* global key bindings *) - (fun (key, callback) -> self#addKeyBinding key callback) + (fun (key, modifiers, callback) -> + self#addKeyBinding key ~modifiers callback) (* [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, toggle_win ~check:main#showCheckMenuItem check#checkWin; *) - [ ]; + [ + GdkKeysyms._Page_Down, [`CONTROL], main#scriptNotebook#next_page; + GdkKeysyms._Page_Up, [`CONTROL], main#scriptNotebook#previous_page + ]; (* about win *) let parse_txt_file file = let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in @@ -453,6 +461,7 @@ class gui () = ~website:"http://matita.cs.unibo.it" () in + ignore(about_dialog#event#connect#delete (fun _ -> true)); ignore(about_dialog#connect#response (fun _ ->about_dialog#misc#hide ())); connect_menu_item main#contentsMenuItem (fun () -> if 0 = Sys.command "which gnome-help" then @@ -508,16 +517,10 @@ class gui () = ~callback:(fun _ -> hide_find_Repl ();true)); connect_menu_item main#undoMenuItem (fun () -> (MatitaScript.current ())#safe_undo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_undo - ~callback:main#undoMenuItem#misc#set_sensitive); -*) main#undoMenuItem#misc#set_sensitive true; + main#undoMenuItem#misc#set_sensitive false; connect_menu_item main#redoMenuItem (fun () -> (MatitaScript.current ())#safe_redo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_redo - ~callback:main#redoMenuItem#misc#set_sensitive); -*) main#redoMenuItem#misc#set_sensitive true; + main#redoMenuItem#misc#set_sensitive false; connect_menu_item main#editMenu (fun () -> main#copyMenuItem#misc#set_sensitive (MatitaScript.current ())#canCopy; @@ -564,7 +567,7 @@ class gui () = GtkThread.sync (fun () -> ()) () in let worker_thread = ref None in - let notify_exn (source_view : GSourceView2.source_view) exn = + let notify_exn (source_view : GSourceView3.source_view) exn = let floc, msg = MatitaExcPp.to_string exn in begin match floc with @@ -589,7 +592,7 @@ class gui () = match !id with | None -> assert false (* a race condition occurred *) | Some id -> - (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id)); + source_view#source_buffer#misc#disconnect id)); source_view#source_buffer#place_cursor (source_view#source_buffer#get_iter (`OFFSET x')); end; @@ -657,32 +660,6 @@ class gui () = with exc -> script#source_view#misc#grab_focus (); raise exc in - (* file selection win *) - ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); - ignore (fileSel#fileSelectionWin#connect#response (fun event -> - let return r = - chosen_file <- r; - fileSel#fileSelectionWin#misc#hide (); - GMain.Main.quit () - in - match event with - | `OK -> - let fname = fileSel#fileSelectionWin#filename in - if Sys.file_exists fname then - begin - if HExtlib.is_regular fname && not (_only_directory) then - return (Some fname) - else if _only_directory && HExtlib.is_dir fname then - return (Some fname) - end - else - begin - if _ok_not_exists then - return (Some fname) - end - | `CANCEL -> return None - | `HELP -> () - | `DELETE_EVENT -> return None)); (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ]; (* console *) @@ -752,7 +729,7 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem ~callback:(function b -> let s = s () in - let status = Interpretations.toggle_active_interpretations s#status b + let _status = Interpretations.toggle_active_interpretations s#status b in assert false (* MATITA 1.0 ??? s#set_grafite_status status*) @@ -765,7 +742,7 @@ class gui () = main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) - HLog.set_log_callback self#console#log_callback; + HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg); GtkSignal.user_handler := (function | MatitaScript.ActionCancelled s -> HLog.error s @@ -861,12 +838,16 @@ class gui () = MatitaMisc.decrease_font_size; connect_menu_item main#normalFontSizeMenuItem MatitaMisc.reset_font_size; - ignore (main#scriptNotebook#connect#switch_page - (fun page -> - let script = MatitaScript.at_page page in - script#activate; - main#saveMenuItem#misc#set_sensitive script#has_name)); - self#newScript () + ignore (main#scriptNotebook#connect#switch_page (fun page -> + self#save_page (); + current_page <- page; + let script = MatitaScript.at_page page in + script#activate; + main#undoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_undo ; + main#redoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_redo ; + main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = let script = MatitaScript.current () in @@ -968,23 +949,28 @@ class gui () = let script = MatitaScript.at_page page in self#closeScript page script - method private newScript () = + method private save_page () = + if current_page >= 0 then + let old_script = MatitaScript.at_page current_page in + save_moo0 ~do_clean:false old_script old_script#status + + method newScript () = + self#save_page (); let scrolledWindow = GBin.scrolled_window () in let hbox = GPack.hbox () in - let tab_label = GMisc.label ~text:"foo" - ~packing:hbox#pack () in + let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in let _ = GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in let closebutton = GButton.button ~relief:`NONE ~packing:hbox#pack () in - let image = - GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in + let image = GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in closebutton#set_image image#coerce; let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce scrolledWindow#coerce); ignore (closebutton#connect#clicked (fun () -> - self#closeScript (main#scriptNotebook#page_num hbox#coerce) script)); + self#closeScript + (main#scriptNotebook#page_num scrolledWindow#coerce) script)); main#scriptNotebook#goto_page 0; sequents_viewer#reset; sequents_viewer#load_logo; @@ -1031,12 +1017,12 @@ class gui () = self#main#saveMenuItem#misc#set_sensitive true method private console = console - method private fileSel = fileSel method private findRepl = findRepl method main = main - method private addKeyBinding key callback = - List.iter (fun evbox -> add_key_binding key callback evbox) + method private addKeyBinding key ?modifiers callback = +(* List.iter (fun evbox -> add_key_binding key callback evbox) *) + List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback) keyBindingBoxes method private setQuitCallback callback = @@ -1045,27 +1031,55 @@ class gui () = (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback + method private chooseFileOrDir ok_not_exists only_directory = + let fileSel = GWindow.file_chooser_dialog + ~action:`OPEN + ~title:"Select file" + ~modal:true + ~type_hint:`DIALOG + ~position:`CENTER + () in + fileSel#add_select_button_stock `OPEN `OK; + fileSel#add_button_stock `CANCEL `CANCEL; + ignore (fileSel#set_current_folder(Sys.getcwd ())) ; + let res = + let rec aux () = + match fileSel#run () with + | `OK -> + (match fileSel#filename with + None -> aux () + | Some fname -> + if Sys.file_exists fname then + begin + if HExtlib.is_regular fname && not (only_directory) then + Some fname + else if only_directory && HExtlib.is_dir fname then + Some fname + else + aux () + end + else if ok_not_exists then Some fname else aux ()) + | `CANCEL -> None + | `DELETE_EVENT -> None in + aux () in + fileSel#destroy () ; + res + method private chooseFile ?(ok_not_exists = false) () = - _ok_not_exists <- ok_not_exists; - _only_directory <- false; - fileSel#fileSelectionWin#show (); - GtkThread.main (); - chosen_file + self#chooseFileOrDir ok_not_exists false 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 + self#chooseFileOrDir ok_not_exists true end let gui () = let g = new gui () in - MatitaMisc.set_gui g; - g + let rg = (g :> MatitaGuiTypes.gui) in + MatitaMisc.set_gui rg; + g#newScript (); + rg let instance = singleton gui @@ -1252,6 +1266,4 @@ let _ = interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) - ignore (GMain.Main.init ()) - + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file (* loads gtk rc *)