X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=d009a63f6f43646846a782265bb276743325e708;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=0bea9c43f6a1531c5bb6d927544e8ecc2e873372;hpb=79ba29ddfc90c0b9bc26e1ddde46cb94cb800d51;p=helm.git diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 0bea9c43f..d009a63f6 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -35,8 +35,6 @@ exception Found of int let all_disambiguation_passes = ref false -let gui_instance = ref None - (* this is a shit and should be changed :-{ *) let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") @@ -106,14 +104,6 @@ let interactive_uri_choice end -class type browserWin = - (* this class exists only because GEdit.combo_box_entry is not supported by - * lablgladecc :-(((( *) -object - inherit MatitaGeneratedGui.browserWin - method browserUri: GEdit.entry -end - class console ~(buffer: GText.buffer) () = object (self) val error_tag = buffer#create_tag [ `FOREGROUND "red" ] @@ -138,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 = @@ -425,19 +419,24 @@ class gui () = val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false + val mutable current_page = 0 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 @@ -599,7 +598,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; @@ -762,7 +761,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*) @@ -835,21 +834,13 @@ class gui () = connect_menu_item main#newMenuItem self#newScript; connect_menu_item main#closeMenuItem self#closeCurrentScript; connect_menu_item main#showCoercionsGraphMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Coercions)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions))); connect_menu_item main#showHintsDbMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Hints)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints))); connect_menu_item main#showTermGrammarMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Grammar)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar))); connect_menu_item main#showUnicodeTable - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `TeX)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX))); (* debug menu *) main#debugMenu#misc#hide (); (* HBUGS *) @@ -872,7 +863,7 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* math view handling *) connect_menu_item main#newCicBrowserMenuItem (fun () -> - ignore(MatitaMathView.cicBrowser ())); + ignore(MatitaMathView.cicBrowser None)); connect_menu_item main#increaseFontSizeMenuItem MatitaMisc.increase_font_size; connect_menu_item main#decreaseFontSizeMenuItem @@ -881,9 +872,12 @@ class gui () = MatitaMisc.reset_font_size; ignore (main#scriptNotebook#connect#switch_page (fun page -> + let old_script = MatitaScript.at_page current_page in + save_moo0 ~do_clean:false old_script old_script#status; + current_page <- page; let script = MatitaScript.at_page page in script#activate; - main#saveMenuItem#misc#set_sensitive script#has_name)); + main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = let script = MatitaScript.current () in @@ -988,20 +982,19 @@ class gui () = method newScript () = 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; @@ -1052,19 +1045,9 @@ class gui () = method private findRepl = findRepl method main = main - method newBrowserWin () = - object (self) - inherit browserWin () - val combo = GEdit.entry () - initializer - let combo_widget = combo#coerce in - uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; - combo#misc#grab_focus () - method browserUri = combo - end - - 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 = @@ -1092,9 +1075,10 @@ class gui () = let gui () = let g = new gui () in - gui_instance := Some g; - MatitaMisc.set_gui g; - g + let rg = (g :> MatitaGuiTypes.gui) in + MatitaMisc.set_gui rg; + g#newScript (); + rg let instance = singleton gui