X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=7161aa9e845c990c34e8cc30eb5b1a9d7a8d464b;hp=16af244349b40bbaf69027b8a83a55663c94b209;hb=b5d69130dd83587b5fb9cbb39251aaa8df8c456e;hpb=9226222b139844ebae3bddd6aef489d60e41e27a diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 16af24434..7161aa9e8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -50,21 +50,17 @@ class gui file = let main = new mainWin ~file () in let about = new aboutWin ~file () in let dialog = new genericDialog ~file () in - let uriChoice = new uriChoiceDialog ~file () in - let interpChoice = new interpChoiceDialog ~file () in let fileSel = new fileSelectionWin ~file () in let proof = new proofWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox ] in - let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in object (self) initializer (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c dialog; c fileSel; c main; c proof; c toolbar; - c uriChoice; c interpChoice ]); + [ c about; c dialog; c fileSel; c main; c proof; c toolbar ]); (* show/hide commands *) toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; toggle_visibility proof#proofWin main#showProofMenuItem; @@ -90,11 +86,19 @@ class gui file = method main = main method about = about method dialog = dialog - method uriChoice = uriChoice - method interpChoice = interpChoice method fileSel = fileSel method proof = proof + method newUriDialog () = + let dialog = new uriChoiceDialog ~file () in + dialog#check_widgets (); + dialog + + method newInterpDialog () = + let dialog = new interpChoiceDialog ~file () in + dialog#check_widgets (); + dialog + method private addKeyBinding key callback = List.iter (fun evbox -> add_key_binding key callback evbox) keyBindingBoxes @@ -104,7 +108,5 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback - method uriChoices = uriChoices - end