From 0a9583936e33eb9d65361537fd1e05168d423d11 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 31 May 2005 13:01:29 +0000
Subject: [PATCH] new shortcuts fixed hint uri chooser

---
 helm/matita/matita.glade    |  8 ++++----
 helm/matita/matita.ml       |  2 +-
 helm/matita/matitaGui.ml    | 16 ++++++++++++----
 helm/matita/matitaGui.mli   |  1 +
 helm/matita/matitaScript.ml |  8 +++++++-
 5 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index c0c4862a3..7ae1860d5 100644
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1871,7 +1871,7 @@ Copyright (C) 2005,
 				  <property name="can_focus">True</property>
 				  <property name="relief">GTK_RELIEF_NONE</property>
 				  <property name="focus_on_click">True</property>
-				  <accelerator key="Home" modifiers="0" signal="clicked"/>
+				  <accelerator key="Home" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
 
 				  <child>
 				    <widget class="GtkImage" id="image253">
@@ -1907,7 +1907,7 @@ Copyright (C) 2005,
 				  <property name="can_focus">True</property>
 				  <property name="relief">GTK_RELIEF_NONE</property>
 				  <property name="focus_on_click">True</property>
-				  <accelerator key="Page_Up" modifiers="0" signal="clicked"/>
+				  <accelerator key="Page_Up" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
 
 				  <child>
 				    <widget class="GtkImage" id="image254">
@@ -1978,7 +1978,7 @@ Copyright (C) 2005,
 				  <property name="can_focus">True</property>
 				  <property name="relief">GTK_RELIEF_NONE</property>
 				  <property name="focus_on_click">True</property>
-				  <accelerator key="Page_Down" modifiers="0" signal="clicked"/>
+				  <accelerator key="Page_Down" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
 
 				  <child>
 				    <widget class="GtkImage" id="image256">
@@ -2014,7 +2014,7 @@ Copyright (C) 2005,
 				  <property name="can_focus">True</property>
 				  <property name="relief">GTK_RELIEF_NONE</property>
 				  <property name="focus_on_click">True</property>
-				  <accelerator key="End" modifiers="0" signal="clicked"/>
+				  <accelerator key="End" modifiers="GDK_CONTROL_MASK" signal="clicked"/>
 
 				  <child>
 				    <widget class="GtkImage" id="image257">
diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index a422ece16..c1225bae4 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -68,7 +68,7 @@ let script =
         MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
         ~title:"Matita: URI chooser" 
         ~msg:"Select the URI" ~hide_uri_entry:true
-        ~hide_try:true ~ok_label:"_Apply" 
+        ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
         ~copy_cb:(fun s -> gui#main#scriptTextView#buffer#insert ("\n"^s^"\n"))
         () ~id:"boh?" uris
       with MatitaTypes.Cancel -> [])
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f3b531fb2..f6cdff77d 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -327,10 +327,12 @@ let is_var_uri s =
     String.sub s (String.length s - 4) 4 = ".var"
   with Invalid_argument _ -> false
 
+(* this is a shit and should be changed :-{ *)
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
-  ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
+  ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) 
+  ?copy_cb ()
   ~id uris
 =
   let gui = instance () in
@@ -375,9 +377,15 @@ let interactive_uri_choice
     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)));
+    if ok_action = `AUTO then
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        Helm_registry.set_bool "matita.auto_disambiguation" true;
+        return (Some (Lazy.force nonvars_uris)))
+    else
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        match model#easy_selection () with
+        | [] -> ()
+        | uris -> return (Some uris));
     connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()
diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index cb2cbeb0c..f517bbb9c 100644
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -88,6 +88,7 @@ val interactive_uri_choice:
   ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
   ?msg:string -> ?nonvars_button:bool -> 
   ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
+  ?ok_action:[`AUTO|`SELECT] ->
   ?copy_cb:(string -> unit) -> unit ->
     MatitaDisambiguator.choose_uris_callback
 
diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 58043bbd3..f9855348a 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -196,7 +196,13 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
           "\n" ^ TAPp.pp_statement ast
         in
         [ new_status , extra_text ], parsed_text_length
-      | _ -> assert false)
+      | _ -> 
+          MatitaLog.error 
+            "The result of the urichooser should be only 1 uri, not:\n";
+          List.iter (
+            fun u -> MatitaLog.error (u ^ "\n")
+          ) selected;
+          assert false)
   | TA.Check (_,term) ->
       let metasenv = MatitaMisc.get_proof_metasenv status in
       let context = MatitaMisc.get_proof_context status in
-- 
2.39.2