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

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index fc4fecc8f..2ff018a52 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -75,3 +75,116 @@ class stringListModel (tree_view: GTree.view) =
 
   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 newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+    method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+  end
+
+exception Cancel
+
+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));
+    ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
+      Helm_registry.set_bool "matita.auto_disambiguation" true;
+      return (Some (Lazy.force nonvars_uris))));
+    ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
+      match model#easy_selection () with
+      | [] -> ()
+      | uris -> return (Some uris)));
+    ignore (dialog#uriChoiceAbortButton#connect#clicked (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 =
+  (* TODO Zack implement interactive_interp_choice *)
+  MatitaTypes.warning
+    "'interactive_interp_choice' not implemented: returning 1st interpretation";
+  [0]
+
+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));
+  ignore (dialog#confirmationDialogOkButton#connect#clicked (return true));
+  ignore (dialog#confirmationDialogCancelButton#connect#clicked (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 ();
+    ignore (dialog#emptyDialogOkButton#connect#clicked (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 ();
+    ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ ->
+      return (Some entry#text)))
+  end;
+  ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None));
+  dialog#emptyDialog#show ();
+  GtkThread.main ();
+  (match !result with None -> raise Cancel | Some r -> r)
+