From 1d39965a694698c3df238fc424203c6b77b067e7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 20:30:15 +0100 Subject: Selecting whole words on double-click in CoqIDE. Fixes bug #4026. --- ide/gtk_parsing.ml | 13 +++++++++++++ ide/wg_MessageView.ml | 1 + ide/wg_ProofView.ml | 1 + ide/wg_ScriptView.ml | 1 + 4 files changed, 16 insertions(+) (limited to 'ide') diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index abbd7e6d59..79ccf61a43 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -166,3 +166,16 @@ let find_nearest_backward (cursor:GText.iter) targets = | None -> raise Not_found | Some nearest -> nearest +(** On double-click on a view, select the whole word. This is a workaround for + a deficient word handling in TextView. *) +let fix_double_click self = + let callback ev = match GdkEvent.get_type ev with + | `TWO_BUTTON_PRESS -> + let iter = self#buffer#get_iter `INSERT in + let start, stop = get_word_around iter in + let () = self#buffer#move_mark `INSERT ~where:start in + let () = self#buffer#move_mark `SEL_BOUND ~where:stop in + true + | _ -> false + in + ignore (self#event#connect#button_press ~callback) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 09f1d44535..b32674084d 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -48,6 +48,7 @@ let message_view () : message_view = ~source_buffer:buffer ~packing:scroll#add ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index a33f2c591c..b12d29d6c9 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -181,6 +181,7 @@ let proof_view () = let view = GSourceView2.source_view ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in object diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 5d21efd956..8298d9954f 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -418,6 +418,7 @@ object (self) self#buffer#end_user_action () initializer + let () = Gtk_parsing.fix_double_click self in let supersed cb _ = let _ = cb () in GtkSignal.stop_emit() -- cgit v1.2.3 From 6b5bc2ceb986913bf28a08dadb1e4ef01a595a3b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 21:02:33 +0100 Subject: CoqIDE now remembers the path of the last opened project. Fixes bug #2762. --- ide/ideutils.ml | 14 ++++++++------ ide/preferences.ml | 4 ++++ ide/preferences.mli | 1 + 3 files changed, 13 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 84ef8f40db..473b8dc82e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -132,8 +132,6 @@ let mktimer () = with Glib.GError _ -> ()); timer := None) } -let last_dir = ref "" - let filter_all_files () = GFile.filter ~name:"All" ~patterns:["*"] () @@ -142,6 +140,10 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () +let current_dir () = match current.project_path with +| None -> "" +| Some dir -> dir + let select_file_for_open ~title () = let file = ref None in let file_chooser = @@ -152,14 +154,14 @@ let select_file_for_open ~title () = file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); file_chooser#set_default_response `OPEN; - ignore (file_chooser#set_current_folder !last_dir); + ignore (file_chooser#set_current_folder (current_dir ())); begin match file_chooser#run () with | `OPEN -> begin file := file_chooser#filename; match !file with | None -> () - | Some s -> last_dir := Filename.dirname s; + | Some s -> current.project_path <- file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; @@ -178,7 +180,7 @@ let select_file_for_save ~title ?filename () = file_chooser#set_do_overwrite_confirmation true; file_chooser#set_default_response `SAVE; let dir,filename = match filename with - |None -> !last_dir, "" + |None -> current_dir (), "" |Some f -> Filename.dirname f, Filename.basename f in ignore (file_chooser#set_current_folder dir); @@ -189,7 +191,7 @@ let select_file_for_save ~title ?filename () = file := file_chooser#filename; match !file with None -> () - | Some s -> last_dir := Filename.dirname s; + | Some s -> current.project_path <- file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; diff --git a/ide/preferences.ml b/ide/preferences.ml index 9a4fde2f6e..d32920ed3f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -105,6 +105,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; @@ -182,6 +183,7 @@ let current = { read_project = Ignore_args; project_file_name = "_CoqProject"; + project_path = None; encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; @@ -265,6 +267,7 @@ let save_pref () = add "project_options" [string_of_project_behavior p.read_project] ++ add "project_file_name" [p.project_file_name] ++ + add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++ add "encoding" [string_of_inputenc p.encoding] ++ @@ -342,6 +345,7 @@ let load_pref () = set_hd "project_options" (fun v -> np.read_project <- (project_behavior_of_string v)); set_hd "project_file_name" (fun v -> np.project_file_name <- v); + set_option "project_path" (fun v -> np.project_path <- v); set "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); diff --git a/ide/preferences.mli b/ide/preferences.mli index ab12e4c7ba..1e4f152c23 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -32,6 +32,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; -- cgit v1.2.3 From cb4ddb3c0421f828f627215aeb64b286c05c617a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 21:58:38 +0100 Subject: Changing default for CoqIDE project to append arguments. Implement wish #3582. --- ide/preferences.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index d32920ed3f..c59642d3a7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -181,7 +181,7 @@ let current = { source_language = "coq"; source_style = "coq_style"; - read_project = Ignore_args; + read_project = Append_args; project_file_name = "_CoqProject"; project_path = None; -- cgit v1.2.3 From 06f980bea466a21be2d1715679a5b6e54dcf7b67 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 15 Feb 2015 22:17:53 +0100 Subject: Fixing bug #4037. --- ide/coqOps.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 689d4908f7..8ba1c8ecd2 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -218,8 +218,15 @@ object(self) let on_click id = let find _ _ s = Int.equal s.index id in let sentence = Doc.find document find in - let mark = sentence.stop in + let mark = sentence.start in let iter = script#buffer#get_iter_at_mark mark in + (** Sentence starts tend to be at the end of a line, so we rather choose + the first non-line-ending position. *) + let rec sentence_start iter = + if iter#ends_line then sentence_start iter#forward_line + else iter + in + let iter = sentence_start iter in script#buffer#place_cursor iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in -- cgit v1.2.3 From 09aab35f45b4da30f2171b7477211fb88ffecd22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Feb 2015 10:12:25 +0100 Subject: CoqIDE: read-only Qed sentence reflected in colors (Close: 4051) --- ide/coqide.ml | 5 +++++ ide/tags.ml | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 5aac8f2a18..29fc27baa7 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1333,6 +1333,11 @@ let build_ui () = (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); Tags.Script.incomplete#set_property (`BACKGROUND_GDK (Tags.get_processed_color ())); + Tags.Script.read_only#set_property + (`BACKGROUND_STIPPLE + (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); + Tags.Script.read_only#set_property + (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () diff --git a/ide/tags.ml b/ide/tags.ml index 079cf94853..d4460b0770 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -52,7 +52,9 @@ struct t let all = edit_zone :: all - let read_only = make_tag table ~name:"read_only" [`EDITABLE false ] + let read_only = make_tag table ~name:"read_only" [`EDITABLE false; + `BACKGROUND !processing_color; + `BACKGROUND_STIPPLE_SET true ] end module Proof = @@ -94,6 +96,7 @@ let set_processing_color clr = let s = string_of_color clr in processing_color := s; Script.incomplete#set_property (`BACKGROUND s); + Script.read_only#set_property (`BACKGROUND s); Script.to_process#set_property (`BACKGROUND s) let get_error_color () = color_of_string !error_color -- cgit v1.2.3 From 52464172064fa66b1bb85d34e0062be04b2ecf97 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Feb 2015 10:19:27 +0100 Subject: Tentative fix for bug #2855. --- ide/coqide.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 29fc27baa7..4ca99256a1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1149,14 +1149,14 @@ let build_ui () = menu templates_menu [ item "Templates" ~label:"Te_mplates"; - template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L"); + template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J"); template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T"); template_item ("Definition ident := .\n", 11,5, "E"); template_item ("Inductive ident : :=\n | : .\n", 10,5, "I"); template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F"); template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^ "with _ := Induction for _ Sort _.\n", 7,10, "S"); - item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"C") + item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M") ~callback:match_callback ]; alpha_items templates_menu "Template" Coq_commands.commands; @@ -1164,12 +1164,12 @@ let build_ui () = let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" (Some "F2"); - qitem "Check" (Some "F3"); - qitem "Print" (Some "F4"); - qitem "About" (Some "F5"); - qitem "Locate" None; - qitem "Print Assumptions" None; + qitem "Search" (Some "K"); + qitem "Check" (Some "C"); + qitem "Print" (Some "P"); + qitem "About" (Some "A"); + qitem "Locate" (Some "L"); + qitem "Print Assumptions" (Some "N"); qitem "Whelp Locate" None; ]; -- cgit v1.2.3 From 8c0bc2f5e51b6037868a4dcab612390e67136be0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Feb 2015 16:03:40 +0100 Subject: Fixing bug #4023 again. --- ide/coqide.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 4ca99256a1..cb05363ddc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -852,6 +852,7 @@ let refresh_editor_prefs () = Tags.set_processing_color (Tags.color_of_string current.processing_color); Tags.set_processed_color (Tags.color_of_string current.processed_color); Tags.set_error_color (Tags.color_of_string current.error_color); + Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; -- cgit v1.2.3 From a91df5fdc60977accd7937eb17b62bd551d3213a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 17 Feb 2015 22:41:26 +0100 Subject: Remove Whelp commands. Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive. --- ide/MacOS/default_accel_map | 1 - ide/coq_commands.ml | 2 -- ide/coqide.ml | 1 - ide/coqide_ui.ml | 1 - 4 files changed, 5 deletions(-) (limited to 'ide') diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb124..47612cdf72 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "/Tactics/Tactic constructor" "") ; (gtk_accel_path "/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "/Templates/Template Identity Coercion" "") -; (gtk_accel_path "/Queries/Whelp Locate" "") (gtk_accel_path "/View/Display all low-level contents" "l") ; (gtk_accel_path "/Tactics/Tactic right" "") ; (gtk_accel_path "/Edit/Find Previous" "F3") diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 995c45c5ae..37e38a5464 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,8 +228,6 @@ let state_preserving = [ "Test Printing Synth"; "Test Printing Wildcard"; - "Whelp Hint"; - "Whelp Locate"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index cb05363ddc..4564d620ea 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1171,7 +1171,6 @@ let build_ui () = qitem "About" (Some "A"); qitem "Locate" (Some "L"); qitem "Print Assumptions" (Some "N"); - qitem "Whelp Locate" None; ]; menu tools_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e78c..edfe28b261 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = - -- cgit v1.2.3