Merge PR #12106: Coqide: Apply style scheme and language settings to the three sourceview buffers.

Ack-by: Zimmi48
Reviewed-by: ppedrot

7 files changed, 41 insertions, 5 deletions

diff --git a/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst
new file mode 100644
index 0000000000..a17e9956b9
--- /dev/null
+++ b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Highlighting style and language settings consistently apply to all three buffers of CoqIDE
+  (`#12106 <https://github.com/coq/coq/pull/12106>`_,
+  by Hugo Herbelin; fixes
+  `#11506 <https://github.com/coq/coq/pull/11506>`_).
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index b1f392c337..a69521c278 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -1,3 +1,5 @@
+.. |GtkSourceView| replace:: :smallcaps:`GtkSourceView`
+
 .. _coqintegrateddevelopmentenvironment:
 
 |Coq| Integrated Development Environment
@@ -158,7 +160,18 @@ presented as a notebook.
 The first section is for selecting the text font used for scripts,
 goal and message windows.
 
-The second and third sections are for controlling colors and style.
+The second and third sections are for controlling colors and style of
+the three main buffers. A predefined |Coq| highlighting style as well
+as standard |GtkSourceView| styles are available. Other styles can be
+added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see
+the general documentation about |GtkSourceView| for the various
+possibilities). Note that the style of the rest of graphical part of
+Coqide is not under the control of |GtkSourceView| but of GTK+ and
+governed by files such as ``settings.ini`` and ``gtk.css`` in
+``$XDG_CONFIG_HOME/gtk-3.0`` or files in
+``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment
+variable ``GTK_THEME`` (search on internet for the various
+possibilities).
 
 The fourth section is for customizing the editor. It includes in
 particular the ability to activate an Emacs mode named
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3b36875e3a..54ef8c7a8a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1293,12 +1293,18 @@ let build_ui () =
   (* Initializing hooks *)
   let refresh_style style =
     let style = style_manager#style_scheme style in
-    let iter_session v = v.script#source_buffer#set_style_scheme style in
+    let iter_session v =
+      v.script#source_buffer#set_style_scheme style;
+      v.proof#source_buffer#set_style_scheme style;
+      v.messages#default_route#source_buffer#set_style_scheme style in
     List.iter iter_session notebook#pages
   in
   let refresh_language lang =
     let lang = lang_manager#language lang in
-    let iter_session v = v.script#source_buffer#set_language lang in
+    let iter_session v =
+      v.script#source_buffer#set_language lang;
+      v.proof#source_buffer#set_language lang;
+      v.messages#default_route#source_buffer#set_language lang in
     List.iter iter_session notebook#pages
   in
   let refresh_toolbar b =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index b99e5f8069..9d97b01a7a 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,6 +28,7 @@ end
 class type message_view =
   object
     inherit GObj.widget
+    method source_buffer : GSourceView3.source_buffer
     method connect : message_view_signals
     method clear : unit
     method add : Pp.t -> unit
@@ -44,7 +45,9 @@ class type message_view =
 let message_view () : message_view =
   let buffer = GSourceView3.source_buffer
     ~highlight_matching_brackets:true
-    ~tag_table:Tags.Message.table ()
+    ~tag_table:Tags.Message.table
+    ?language:(lang_manager#language source_language#get)
+    ?style_scheme:(style_manager#style_scheme source_style#get) ()
   in
   let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in
   let box = GPack.vbox () in
@@ -88,6 +91,8 @@ let message_view () : message_view =
 
     val push = new GUtil.signal ()
 
+    method source_buffer = buffer
+
     method connect =
       new message_view_signals_impl box#as_widget push
 
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 21c11b2754..054dd0e571 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,6 +18,7 @@ end
 class type message_view =
   object
     inherit GObj.widget
+    method source_buffer : GSourceView3.source_buffer
     method connect : message_view_signals
     method clear : unit
     method add : Pp.t -> unit
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 3e03ef11f7..b8ed3436ce 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -15,6 +15,7 @@ open Ideutils
 class type proof_view =
   object
     inherit GObj.widget
+    method source_buffer : GSourceView3.source_buffer
     method buffer : GText.buffer
     method refresh : force:bool -> unit
     method clear : unit -> unit
@@ -195,7 +196,9 @@ let display mode (view : #GText.view_skel) goals hints evars =
 let proof_view () =
   let buffer = GSourceView3.source_buffer
     ~highlight_matching_brackets:true
-    ~tag_table:Tags.Proof.table ()
+    ~tag_table:Tags.Proof.table
+    ?language:(lang_manager#language source_language#get)
+    ?style_scheme:(style_manager#style_scheme source_style#get) ()
   in
   let text_buffer = new GText.buffer buffer#as_buffer in
   let view = GSourceView3.source_view
@@ -217,6 +220,8 @@ let proof_view () =
     val mutable evars = None
     val mutable last_width = -1
 
+    method source_buffer = buffer
+
     method buffer = text_buffer
 
     method clear () = buffer#set_text ""
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index db6fb9e9cd..8217f72066 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -11,6 +11,7 @@
 class type proof_view =
   object
     inherit GObj.widget
+    method source_buffer : GSourceView3.source_buffer
     method buffer : GText.buffer
     method refresh : force:bool -> unit
     method clear : unit -> unit