From cf4645acc78a8463fa533756efd9a8d9855d727d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Feb 2015 16:09:01 +0100
Subject: Fixing bug #4023.
---
ide/coqide.ml | 5 +++--
ide/preferences.ml | 5 +----
2 files changed, 4 insertions(+), 6 deletions(-)
(limited to 'ide')
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fa64defabd..78fcbaf8cf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -838,6 +838,9 @@ let refresh_editor_prefs () =
sn.command#refresh_font ();
(* Colors *)
+ 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);
sn.script#misc#modify_base [`NORMAL, `COLOR clr];
sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
@@ -1314,8 +1317,6 @@ let build_ui () =
refresh_tabs_hook := refresh_notebook_pos;
(* Color configuration *)
- Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
- Tags.set_processed_color (Tags.color_of_string prefs.processed_color);
Tags.Script.incomplete#set_property
(`BACKGROUND_STIPPLE
(Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c850613253..25712f951b 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -503,10 +503,7 @@ let configure ?(apply=(fun () -> ())) () =
current.processing_color <- Tags.string_of_color processing_button#color;
current.processed_color <- Tags.string_of_color processed_button#color;
current.error_color <- Tags.string_of_color error_button#color;
- !refresh_editor_hook ();
- Tags.set_processing_color processing_button#color;
- Tags.set_processed_color processed_button#color;
- Tags.set_error_color error_button#color
+ !refresh_editor_hook ()
in
custom ~label box callback true
in
--
cgit v1.2.3
From e9b239881bc32dd15ac53b9463708030c95a9e0c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Feb 2015 18:54:10 +0100
Subject: Focussing on message view in CoqIDE when a message is pushed.
Also fixes bug #4030.
---
ide/session.ml | 16 ++++++++++++----
ide/wg_MessageView.ml | 24 +++++++++++++++++++++++-
ide/wg_MessageView.mli | 8 ++++++++
3 files changed, 43 insertions(+), 5 deletions(-)
(limited to 'ide')
diff --git a/ide/session.ml b/ide/session.ml
index 2936321128..072ae61c68 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -465,7 +465,7 @@ let build_layout (sn:session) =
message_frame#misc#show ();
detachable#show);
detachable#button#misc#hide ();
- lbl in
+ detachable, lbl in
let session_tab = GPack.hbox ~homogeneous:false () in
let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
~packing:session_tab#pack () in
@@ -496,9 +496,17 @@ let build_layout (sn:session) =
sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
script_scroll#add sn.script#coerce;
proof_scroll#add sn.proof#coerce;
- ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce);
- let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
- ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce);
+ let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+ let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
+ let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
+ (** When a message is received, focus on the message pane *)
+ let _ =
+ sn.messages#connect#pushed ~callback:(fun _ _ ->
+ let num = message_frame#page_num detach#coerce in
+ if 0 <= num then message_frame#goto_page num
+ )
+ in
+ (** When an error occurs, paint the error label in red *)
let txt = label#text in
let red s = "" ^ s ^ "" in
sn.errpage#on_update ~callback:(fun l ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 9acda53fc3..09f1d44535 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -6,9 +6,25 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+class type message_view_signals =
+object
+ inherit GObj.misc_signals
+ inherit GUtil.add_ml_signals
+ method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
+class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
+object
+ val after = false
+ inherit GObj.misc_signals obj
+ inherit GUtil.add_ml_signals obj [pushed#disconnect]
+ method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s)
+end
+
class type message_view =
object
inherit GObj.widget
+ method connect : message_view_signals
method clear : unit
method add : string -> unit
method set : string -> unit
@@ -38,6 +54,11 @@ let message_view () : message_view =
object (self)
inherit GObj.widget box#as_widget
+ val push = new GUtil.signal ()
+
+ method connect =
+ new message_view_signals_impl box#as_widget push
+
method clear =
buffer#set_text ""
@@ -49,7 +70,8 @@ let message_view () : message_view =
in
if msg <> "" then begin
buffer#insert ~tags msg;
- buffer#insert ~tags "\n"
+ buffer#insert ~tags "\n";
+ push#call (level, msg)
end
method add msg = self#push Pp.Notice msg
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index cd3f00c97d..4dcd7306ba 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -6,9 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+class type message_view_signals =
+object
+ inherit GObj.misc_signals
+ inherit GUtil.add_ml_signals
+ method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
class type message_view =
object
inherit GObj.widget
+ method connect : message_view_signals
method clear : unit
method add : string -> unit
method set : string -> unit
--
cgit v1.2.3
From 154bb6a5134c35caea187b83334c098dbadb4e48 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Feb 2015 19:43:08 +0100
Subject: Fixing bug #3261.
---
ide/coqide.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
(limited to 'ide')
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 78fcbaf8cf..1d76ceada4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -591,10 +591,12 @@ let get_current_word term =
if term.script#buffer#has_selection then
let (start, stop) = term.script#buffer#selection_bounds in
term.script#buffer#get_text ~slice:true ~start ~stop ()
- (** Otherwise try to recover the clipboard *)
- else match Ideutils.cb#text with
- | Some t -> t
- | None -> ""
+ (** Otherwise try to find the word around the cursor *)
+ else
+ let it = term.script#buffer#get_iter_at_mark `INSERT in
+ let start = find_word_start it in
+ let stop = find_word_end start in
+ term.script#buffer#get_text ~slice:true ~start ~stop ()
let print_branch c l =
Format.fprintf c " | @[%a@]=> _@\n"
--
cgit v1.2.3
From 69212fa135879b8df4cf3347a6bee0af769a3ee7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Feb 2015 22:07:32 +0100
Subject: Tentative fix for CoqIDE randomly dropping deletions.
We make the deletion callback not to regenerate a task id, as the insertion
callback does. I can't find a particular reason for this dissymetry, and it
was indeed causing trouble.
---
ide/session.ml | 1 -
1 file changed, 1 deletion(-)
(limited to 'ide')
diff --git a/ide/session.ml b/ide/session.ml
index 072ae61c68..47b747dae7 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -160,7 +160,6 @@ let set_buffer_handlers
end end in
let delete_cb ~start ~stop =
Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
- cur_action := new_action_id ();
let min_iter, max_iter =
if start#compare stop < 0 then start, stop else stop, start in
let text_mark = add_mark min_iter in
--
cgit v1.2.3
From 7c9938cfbd0cf9093f90b0ee7b856105528c2a87 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 Feb 2015 00:53:44 +0100
Subject: Trying to fix bug #3930.
Instead of setting the last modified part of the text to be the insert point,
we register all modifications to the buffer between to user actions and take
the last modified point to be the least offset of all those modifications.
---
ide/session.ml | 7 +++++++
1 file changed, 7 insertions(+)
(limited to 'ide')
diff --git a/ide/session.ml b/ide/session.ml
index 47b747dae7..dc79fa7905 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -133,6 +133,11 @@ let set_buffer_handlers
try ignore(buffer#get_mark (`NAME "stop_of_input"))
with GText.No_such_mark _ -> assert false in
let get_insert () = buffer#get_iter_at_mark `INSERT in
+ let update_prev it =
+ let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
+ if it#offset < prev#offset then
+ buffer#move_mark (`NAME "prev_insert") ~where:it
+ in
let debug_edit_zone () = if false (*!Minilib.debug*) then begin
buffer#remove_tag Tags.Script.edit_zone
~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -147,6 +152,7 @@ let set_buffer_handlers
let insert_cb it s = if String.length s = 0 then () else begin
Minilib.log ("insert_cb " ^ string_of_int it#offset);
let text_mark = add_mark it in
+ let () = update_prev it in
if it#has_tag Tags.Script.to_process then
cancel_signal "Altering the script being processed in not implemented"
else if it#has_tag Tags.Script.read_only then
@@ -162,6 +168,7 @@ let set_buffer_handlers
Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
let min_iter, max_iter =
if start#compare stop < 0 then start, stop else stop, start in
+ let () = update_prev min_iter in
let text_mark = add_mark min_iter in
let rec aux min_iter =
if min_iter#equal max_iter then ()
--
cgit v1.2.3
From 8f73830d46d985906deadae3059db75772281516 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 Feb 2015 11:14:54 +0100
Subject: Selection of the current word in CoqIDE looks at all buffers.
---
ide/coqide.ml | 15 ++++++++++++---
ide/wg_ProofView.ml | 4 ++++
ide/wg_ProofView.mli | 1 +
3 files changed, 17 insertions(+), 3 deletions(-)
(limited to 'ide')
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1d76ceada4..5aac8f2a18 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -588,9 +588,18 @@ let get_current_word term =
| Some p -> p
| None ->
(** Then look at the current selected word *)
- if term.script#buffer#has_selection then
- let (start, stop) = term.script#buffer#selection_bounds in
- term.script#buffer#get_text ~slice:true ~start ~stop ()
+ let buf1 = term.script#buffer in
+ let buf2 = term.proof#buffer in
+ let buf3 = term.messages#buffer in
+ if buf1#has_selection then
+ let (start, stop) = buf1#selection_bounds in
+ buf1#get_text ~slice:true ~start ~stop ()
+ else if buf2#has_selection then
+ let (start, stop) = buf2#selection_bounds in
+ buf2#get_text ~slice:true ~start ~stop ()
+ else if buf3#has_selection then
+ let (start, stop) = buf3#selection_bounds in
+ buf3#get_text ~slice:true ~start ~stop ()
(** Otherwise try to find the word around the cursor *)
else
let it = term.script#buffer#get_iter_at_mark `INSERT in
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 7e7a311ed0..a33f2c591c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -9,6 +9,7 @@
class type proof_view =
object
inherit GObj.widget
+ method buffer : GText.buffer
method refresh : unit -> unit
method clear : unit -> unit
method set_goals : Interface.goals option -> unit
@@ -176,6 +177,7 @@ let proof_view () =
~highlight_matching_brackets:true
~tag_table:Tags.Proof.table ()
in
+ let text_buffer = new GText.buffer buffer#as_buffer in
let view = GSourceView2.source_view
~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
in
@@ -186,6 +188,8 @@ let proof_view () =
val mutable goals = None
val mutable evars = None
+ method buffer = text_buffer
+
method clear () = buffer#set_text ""
method set_goals gls = goals <- gls
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index 1fbf9900ca..c5e042ea52 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -9,6 +9,7 @@
class type proof_view =
object
inherit GObj.widget
+ method buffer : GText.buffer
method refresh : unit -> unit
method clear : unit -> unit
method set_goals : Interface.goals option -> unit
--
cgit v1.2.3