snapshot, notably:

[helm.git] / helm / matita / matitaGtkMisc.ml

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 2ff018a525586b973b20e2498272a1703472950a..874c75c590a8a9ee04d73380dae16ea553cb7152 100644 (file)
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -23,6 +23,10 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
+open MatitaTypes
+
 let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) =
   ignore (check#connect#toggled (fun _ ->
     if check#active then win#show () else win#misc#hide ()));
@@ -75,6 +79,54 @@ class stringListModel (tree_view: GTree.view) =
 
   end
 
+class interpModel =
+  let cols = new GTree.column_list in
+  let id_col = cols#add Gobject.Data.string in
+  let dsc_col = cols#add Gobject.Data.string in
+  let interp_no_col = cols#add Gobject.Data.int in
+  let tree_store = GTree.tree_store cols in
+  let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+  let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+  let id_view_col = GTree.view_column ~renderer:id_renderer () in
+  let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+  fun tree_view choices ->
+    object
+      initializer
+        tree_view#set_model (Some (tree_store :> GTree.model));
+        ignore (tree_view#append_column id_view_col);
+        ignore (tree_view#append_column dsc_view_col);
+        let name_of_interp =
+          (* try to find a reasonable name for an interpretation *)
+          let idx = ref 0 in
+          fun interp ->
+            try
+              List.assoc "0" interp
+            with Not_found ->
+              incr idx; string_of_int !idx
+        in
+        tree_store#clear ();
+        let idx = ref ~-1 in
+        List.iter
+          (fun interp ->
+            incr idx;
+            let interp_row = tree_store#append () in
+            tree_store#set ~row:interp_row ~column:id_col
+              (name_of_interp interp);
+            tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+            List.iter
+              (fun (id, dsc) ->
+                let row = tree_store#append ~parent:interp_row () in
+                tree_store#set ~row ~column:id_col id;
+                tree_store#set ~row ~column:dsc_col dsc;
+                tree_store#set ~row ~column:interp_no_col !idx)
+              interp)
+          choices
+
+      method get_interp_no tree_path =
+        let iter = tree_store#get_iter tree_path in
+        tree_store#get ~row:iter ~column:interp_no_col
+    end
+
 let is_var_uri s =
   try
     String.sub s (String.length s - 4) 4 = ".var"
@@ -84,9 +136,10 @@ let non p x = not (p x)
 
 class type gui =
   object
-    method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+    method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
+    method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
     method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
-    method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+    method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
   end
 
 exception Cancel
@@ -135,10 +188,34 @@ let interactive_user_uri_choice
   end
 
 let interactive_interp_choice ~(gui:#gui) choices =
-  (* TODO Zack implement interactive_interp_choice *)
-  MatitaTypes.warning
-    "'interactive_interp_choice' not implemented: returning 1st interpretation";
-  [0]
+  assert (choices <> []);
+  let dialog = gui#newInterpDialog () in
+  let model = new interpModel dialog#interpChoiceTreeView choices in
+  let interp_len = List.length (List.hd choices) in
+  dialog#interpChoiceDialog#set_title "Interpretation choice";
+  dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+  let interp_no = ref None in
+  let return _ =
+    dialog#interpChoiceDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
+  ignore (dialog#interpChoiceOkButton#connect#clicked (fun _ ->
+    match !interp_no with None -> () | Some _ -> return ()));
+  ignore (dialog#interpChoiceCancelButton#connect#clicked return);
+  ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+    interp_no := Some (model#get_interp_no path);
+    return ()));
+  let selection = dialog#interpChoiceTreeView#selection in
+  ignore (selection#connect#changed (fun _ ->
+    match selection#get_selected_rows with
+    | [path] ->
+        debug_print (sprintf "selection: %d" (model#get_interp_no path));
+        interp_no := Some (model#get_interp_no path)
+    | _ -> assert false));
+  dialog#interpChoiceDialog#show ();
+  GtkThread.main ();
+  (match !interp_no with Some row -> [row] | _ -> raise Cancel)
 
 let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
   let dialog = gui#newConfirmationDialog () in