From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2000 17:07:34 +0000 (+0000) Subject: Code clean-up: only one procedure to create the gtk trees. X-Git-Tag: nogzip~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=162045c913602277d58d5d3b4111d28456e26c19;p=helm.git Code clean-up: only one procedure to create the gtk trees. --- diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 5cd0faf0c..a50555fd8 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -260,29 +260,13 @@ let selection_changed rendering_window uri () = update_output rendering_window uri' ;; -(* CSC: unificare con la creazione la prima volta *) -let rec updateb_pressed theory_rendering_window rendering_window - (sw1, sw ,(hbox : GPack.box)) mktree () -= - Getter.update () ; - (* let's empty the uri trees and rebuild them *) - uritree := [] ; - theoryuritree := [] ; - build_uri_tree () ; - hbox#remove !sw1#coerce ; - hbox#remove !sw#coerce ; - +let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree = let sw3 = GBin.scrolled_window ~width:250 ~height:600 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let tree1 = GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in - sw1 := sw3 ; - ignore(tree_item1#connect#select - (theory_selection_changed theory_rendering_window None)) ; - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)) ; let sw2 = GBin.scrolled_window ~width:250 ~height:600 @@ -290,9 +274,32 @@ let rec updateb_pressed theory_rendering_window rendering_window let tree = GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in - sw := sw2 ; + ignore(tree_item#connect#select (selection_changed rendering_window None)) ; - mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) + mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ; + + ignore(tree_item1#connect#select + (theory_selection_changed theory_rendering_window None)) ; + mktree theory_selection_changed theory_rendering_window tree_item1 + (Dir ("theory:/",theoryuritree)) ; + (sw3,sw2) +;; + +let updateb_pressed theory_rendering_window rendering_window + (sw1, sw ,(hbox : GPack.box)) mktree () += + Getter.update () ; + (* let's empty the uri trees and rebuild them *) + uritree := [] ; + theoryuritree := [] ; + build_uri_tree () ; + hbox#remove !sw1#coerce ; + hbox#remove !sw#coerce ; + let (sw3,sw2) = + create_gtk_trees hbox rendering_window theory_rendering_window mktree + in + sw1 := sw3 ; + sw := sw2 ;; let theory_check rendering_window () = @@ -726,18 +733,9 @@ class selection_window theory_rendering_window rendering_window = let win = GWindow.window ~title:"Known uris" ~border_width:2 () in let vbox = GPack.vbox ~packing:win#add () in let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in - let sw1 = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree1 = - GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in - let tree_item1 = - GTree.tree_item ~label:theorylabel ~packing:tree1#append () in - let sw = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree = - GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in - let tree_item = - GTree.tree_item ~label:label ~packing:tree#append () in + let (sw1,sw) = + create_gtk_trees hbox1 rendering_window theory_rendering_window mktree + in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let updateb = @@ -749,16 +747,7 @@ class selection_window theory_rendering_window rendering_window = object (self) method show () = win#show () initializer - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)); - mktree selection_changed rendering_window tree_item - (Dir ("cic:/",uritree)); - (* signal handlers here *) - ignore (tree_item1#connect#select - ~callback:(theory_selection_changed theory_rendering_window None)) ; - ignore (tree_item#connect#select - ~callback:(selection_changed rendering_window None)) ; ignore (win#connect#destroy ~callback:GMain.Main.quit) ; ignore (quitb#connect#clicked GMain.Main.quit) ; ignore(updateb#connect#clicked (updateb_pressed