From: Enrico Tassi Date: Tue, 31 May 2005 13:01:29 +0000 (+0000) Subject: new shortcuts X-Git-Tag: PRE_INDEX_1~91 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a9583936e33eb9d65361537fd1e05168d423d11;p=helm.git new shortcuts fixed hint uri chooser --- 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, True GTK_RELIEF_NONE True - + @@ -1907,7 +1907,7 @@ Copyright (C) 2005, True GTK_RELIEF_NONE True - + @@ -1978,7 +1978,7 @@ Copyright (C) 2005, True GTK_RELIEF_NONE True - + @@ -2014,7 +2014,7 @@ Copyright (C) 2005, True GTK_RELIEF_NONE True - + 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