]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
- handles about:* uris in cicBrowser
[helm.git] / helm / matita / matitaGui.ml
index d18b82d140833f1cedfdc78db10d728f6af639cb..a17b9bfb16942a8c62ba3cda6f6a186f8824fbad 100644 (file)
@@ -31,6 +31,14 @@ open MatitaMisc
 
 let gui_instance = ref None ;;
 
+class type browserWin =
+  (* this class exists only because GEdit.combo_box_entry is not supported by
+   * lablgladecc :-(((( *)
+object
+  inherit MatitaGeneratedGui.browserWin
+  method browserUri: GEdit.combo_box_entry
+end
+
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
@@ -275,9 +283,16 @@ class gui () =
     method main = main
 
     method newBrowserWin () =
-      let win = new browserWin () in
-      win#check_widgets ();
-      win
+      object (self)
+        inherit browserWin ()
+        val combo = GEdit.combo_box_entry ()
+        initializer
+          self#check_widgets ();
+          let combo_widget = combo#coerce in
+          browserHBox#add combo_widget;
+          browserHBox#reorder_child combo_widget ~pos:6
+        method browserUri = combo
+      end
 
     method newUriDialog () =
       let dialog = new uriChoiceDialog () in