X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathita%2FmathitaGtkMisc.ml;h=fc4fecc8f14154080105e78e991faf65b00809ac;hb=07287062d5b84a0f2b66380d0d380bbf68217a27;hp=36478d5292bf537d01a1166571a1ce18cedd3f6e;hpb=9c70cabfe7bcf809e746f2499902aa7f2f45ca6a;p=helm.git

diff --git a/helm/mathita/mathitaGtkMisc.ml b/helm/mathita/mathitaGtkMisc.ml
index 36478d529..fc4fecc8f 100644
--- a/helm/mathita/mathitaGtkMisc.ml
+++ b/helm/mathita/mathitaGtkMisc.ml
@@ -44,3 +44,34 @@ let add_key_binding key callback (evbox: GBin.event_box) =
         false
     | _ -> false))
 
+class stringListModel (tree_view: GTree.view) =
+  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
+  object (self)
+
+    initializer
+      let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+      let view_column = GTree.view_column ~renderer () in
+      tree_view#set_model (Some (list_store :> GTree.model));
+      ignore (tree_view#append_column view_column)
+
+    method list_store = list_store
+
+    method easy_append s =
+      let tree_iter = list_store#append () in
+      list_store#set ~row:tree_iter ~column:text_column s
+
+    method easy_insert pos s =
+      let tree_iter = list_store#insert pos in
+      list_store#set ~row:tree_iter ~column:text_column s
+
+    method easy_selection () =
+      List.map
+        (fun tree_path ->
+          let iter = list_store#get_iter tree_path in
+          list_store#get ~row:iter ~column:text_column)
+        tree_view#selection#get_selected_rows
+
+  end
+