new shortcuts

fixed hint uri chooser

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index c0c4862a3466c27378086ace0e1b9e46ed992bfa..7ae1860d5361cc2793561748f6d09e7806b40496 100644 (file)
--- 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 a422ece1655ba7321d9ce31d1cb5fb68aaf74d0a..c1225bae46f6b7787b58fe2a1e80a0b739314ddb 100644 (file)
--- 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 f3b531fb285dee2bc6e60e46044fe1e5177acc12..f6cdff77d86b6798b6403b3155f19e1dd9fff811 100644 (file)
--- 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 cb2cbeb0c00ef46775cb549b4d54b8d62d7d538c..f517bbb9cb3c59415cc6e87933e353af687e3ec5 100644 (file)
--- 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 58043bbd3d5acb44ab3af00adb206135c8f12f24..f9855348a0d0ff9b6a4cc8224fd303aa527936e3 100644 (file)
--- 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