X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=aebd2dbc9e536859514474c428abd2bdfeca7906;hb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;hp=fc4fecc8f14154080105e78e991faf65b00809ac;hpb=c5d4ad1c98c1434b95a8a9b1c8697dd36cf39623;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index fc4fecc8f..aebd2dbc9 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -23,6 +23,13 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
+open MatitaTypes
+
+let connect_button (button: GButton.button) callback =
+  ignore (button#connect#clicked callback)
+
 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,3 +82,188 @@ 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"
+  with Invalid_argument _ -> false
+
+let non p x = not (p x)
+
+class type gui =
+  object
+    method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
+    method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
+    method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+    method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
+  end
+
+let interactive_user_uri_choice
+  ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "")
+  ?(msg = "") ?(nonvars_button=false) uris
+=
+  let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
+  if (selection_mode <> `SINGLE) &&
+    (Helm_registry.get_bool "matita.auto_disambiguation")
+  then
+    Lazy.force nonvars_uris
+  else begin
+    let dialog = gui#newUriDialog () in
+    dialog#uriChoiceTreeView#selection#set_mode
+      (selection_mode :> Gtk.Tags.selection_mode);
+    let model = new stringListModel dialog#uriChoiceTreeView in
+    let choices = ref None in
+    let nonvars = ref false in
+    dialog#uriChoiceDialog#set_title title;
+    dialog#uriChoiceLabel#set_text msg;
+    List.iter model#easy_append uris;
+    dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+    let return v =
+      choices := v;
+      dialog#uriChoiceDialog#destroy ();
+      GMain.Main.quit ()
+    in
+    ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+    connect_button dialog#uriChoiceConstantsButton (fun _ ->
+      return (Some (Lazy.force nonvars_uris)));
+    connect_button dialog#uriChoiceAutoButton (fun _ ->
+      Helm_registry.set_bool "matita.auto_disambiguation" true;
+      return (Some (Lazy.force nonvars_uris)));
+    connect_button dialog#uriChoiceSelectedButton (fun _ ->
+      match model#easy_selection () with
+      | [] -> ()
+      | uris -> return (Some uris));
+    connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+    dialog#uriChoiceDialog#show ();
+    GtkThread.main ();
+    (match !choices with 
+    | None -> raise Cancel
+    | Some uris -> uris)
+  end
+
+let interactive_interp_choice ~(gui:#gui) choices =
+  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
+  let fail _ = interp_no := None; return () in
+  ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
+  connect_button dialog#interpChoiceOkButton (fun _ ->
+    match !interp_no with None -> () | Some _ -> return ());
+  connect_button dialog#interpChoiceCancelButton fail;
+  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
+  dialog#confirmationDialog#set_title title;
+  dialog#confirmationDialogLabel#set_label msg;
+  let result = ref None in
+  let return r _ =
+    result := Some r;
+    dialog#confirmationDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
+  connect_button dialog#confirmationDialogOkButton (return true);
+  connect_button dialog#confirmationDialogCancelButton (return false);
+  dialog#confirmationDialog#show ();
+  GtkThread.main ();
+  (match !result with None -> assert false | Some r -> r)
+
+let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
+  let dialog = gui#newEmptyDialog () in
+  dialog#emptyDialog#set_title title;
+  dialog#emptyDialogLabel#set_label msg;
+  let result = ref None in
+  let return r =
+    result := r;
+    dialog#emptyDialog#destroy ();
+    GMain.Main.quit ()
+  in
+  ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true));
+  if multiline then begin (* multiline input required: use a TextView widget *)
+    let win =
+      GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER
+        ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add ()
+    in
+    let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
+    view#misc#grab_focus ();
+    connect_button dialog#emptyDialogOkButton (fun _ ->
+      return (Some (view#buffer#get_text ())))
+  end else begin (* monoline input required: use a TextEntry widget *)
+    let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
+    entry#misc#grab_focus ();
+    connect_button dialog#emptyDialogOkButton (fun _ ->
+      return (Some entry#text))
+  end;
+  connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
+  dialog#emptyDialog#show ();
+  GtkThread.main ();
+  (match !result with None -> raise Cancel | Some r -> r)
+