X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=de5240e447ccacbf533609fe91f6b59f44e49f09;hb=3c9c376401844c389d682ba835845443105e4b1a;hp=26cf9df086cacdd54511d0ded7bb5dab02fa40b0;hpb=e35ec00b1be70e4b064b74a49735b37b5e719e5b;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 26cf9df08..de5240e44 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -23,24 +23,6 @@ * http://helm.cs.unibo.it/ *) -(* -class stringListModel' uriChoiceDialog = - let tree_view = uriChoiceDialog#uriChoiceTreeView in - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - let _ = tree_view#set_model (Some (list_store :> GTree.model)) in - let _ = tree_view#append_column view_column in - object - method append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - method clear () = list_store#clear () - end -*) - open Printf open MatitaGeneratedGui @@ -56,9 +38,12 @@ class gui file = let proof = new proofWin ~file () in let check = new checkWin ~file () in let script = new scriptWin ~file () in + let browser = new browserWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; - check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ] + check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox; + browser#browserWinEventBox + ] in let console = MatitaConsole.console ~evbox:main#consoleEventBox @@ -80,9 +65,11 @@ class gui file = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]); - (* "global" key bindings *) - List.iter (fun (key, callback) -> self#addKeyBinding key callback) + [ c about; c fileSel; c main; c proof; c toolbar; c check; c script; + c browser ]); + (* key bindings *) + List.iter (* global key bindings *) + (fun (key, callback) -> self#addKeyBinding key callback) [ GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin; GdkKeysyms._F4, @@ -91,6 +78,7 @@ class gui file = toggle_win ~check:main#showScriptMenuItem script#scriptWin; GdkKeysyms._x, (fun () -> console#toggle ()); ]; + add_key_binding GdkKeysyms._Escape console#hide main#consoleEventBox; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); ignore (main#aboutMenuItem#connect#activate (fun _ -> @@ -135,6 +123,7 @@ class gui file = *) method about = about + method browser = browser method check = check method console = console method fileSel = fileSel