Code clean-up: only one procedure to create the gtk trees.

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 5cd0faf0c999460cb0b7f67b0578758b46c4d80c..a50555fd8a8b6fdcb2f76cb115d2dd1d4d80bfa0 100755 (executable)
--- 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