aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml5
-rw-r--r--ide/coqide_WIN32.ml.in3
-rw-r--r--ide/idetop.ml20
-rw-r--r--ide/wg_MessageView.ml6
-rw-r--r--ide/wg_MessageView.mli1
-rw-r--r--ide/wg_ProofView.ml6
-rw-r--r--ide/wg_ProofView.mli1
7 files changed, 28 insertions, 14 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3b36875e3a..ab2a17798e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1293,7 +1293,10 @@ 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 =
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in
index 2d3964f210..be8aab9e49 100644
--- a/ide/coqide_WIN32.ml.in
+++ b/ide/coqide_WIN32.ml.in
@@ -44,6 +44,7 @@ let () =
Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
set_win32_path ();
Coq.interrupter := win32_interrupt;
- reroute_stdout_stderr ()
+ reroute_stdout_stderr ();
+ try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0"
let init () = ()
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 0ef7fca41f..fa458e7c6e 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -232,32 +232,32 @@ let goals () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
try
- let newp = Vernacstate.Proof_global.give_me_the_proof () in
+ let newp = Vernacstate.Declare.give_me_the_proof () in
if Proof_diffs.show_diffs () then begin
let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
end else
Some (export_pre_goals Proof.(data newp) process_goal)
- with Vernacstate.Proof_global.NoCurrentProof -> None
+ with Vernacstate.Declare.NoCurrentProof -> None
[@@ocaml.warning "-3"];;
let evars () =
try
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
- let pfts = Vernacstate.Proof_global.give_me_the_proof () in
+ let pfts = Vernacstate.Declare.give_me_the_proof () in
let Proof.{ sigma } = Proof.data pfts in
let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
let el = List.map map_evar exl in
Some el
- with Vernacstate.Proof_global.NoCurrentProof -> None
+ with Vernacstate.Declare.NoCurrentProof -> None
[@@ocaml.warning "-3"]
let hints () =
try
- let pfts = Vernacstate.Proof_global.give_me_the_proof () in
+ let pfts = Vernacstate.Declare.give_me_the_proof () in
let Proof.{ goals; sigma } = Proof.data pfts in
match goals with
| [] -> None
@@ -266,7 +266,7 @@ let hints () =
let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
Some (hint_hyps, concl_next_tac)
- with Vernacstate.Proof_global.NoCurrentProof -> None
+ with Vernacstate.Declare.NoCurrentProof -> None
[@@ocaml.warning "-3"]
(** Other API calls *)
@@ -287,11 +287,11 @@ let status force =
List.rev_map Names.Id.to_string l
in
let proof =
- try Some (Names.Id.to_string (Vernacstate.Proof_global.get_current_proof_name ()))
- with Vernacstate.Proof_global.NoCurrentProof -> None
+ try Some (Names.Id.to_string (Vernacstate.Declare.get_current_proof_name ()))
+ with Vernacstate.Declare.NoCurrentProof -> None
in
let allproofs =
- let l = Vernacstate.Proof_global.get_all_proof_names () in
+ let l = Vernacstate.Declare.get_all_proof_names () in
List.map Names.Id.to_string l
in
{
@@ -340,7 +340,7 @@ let import_search_constraint = function
| Interface.Include_Blacklist -> Search.Include_Blacklist
let search flags =
- let pstate = Vernacstate.Proof_global.get_pstate () in
+ let pstate = Vernacstate.Declare.get_pstate () in
List.map export_coq_object (Search.interface_search ?pstate (
List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
)
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index b99e5f8069..6e22172d05 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,8 @@ 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
+ ?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 +90,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..1de63953af 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,8 @@ 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
+ ?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 +219,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:38:18 +0000