Coqide: Apply style scheme and language to the three buffers.

It was previously only applied to the script buffer.

5 files changed, 22 insertions, 4 deletions

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