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/session.ml2
-rw-r--r--ide/wg_Completion.ml20
-rw-r--r--ide/wg_Completion.mli2
-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
-rw-r--r--ide/wg_ScriptView.ml2
10 files changed, 28 insertions, 20 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/session.ml b/ide/session.ml
index b16af9c317..09391b7f50 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -151,7 +151,7 @@ let set_buffer_handlers
else if it#has_tag Tags.Script.processed then Some old
else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
else None in
- aux it it in
+ aux it it#copy in
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
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index dcb71d96a1..cc24e71386 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -69,7 +69,7 @@ let is_substring s1 s2 =
if !break then len2 - len1
else -1
-class completion_provider coqtop =
+class completion_provider buffer coqtop =
let self_provider = ref None in
let active = ref true in
let provider = object (self)
@@ -97,9 +97,13 @@ class completion_provider coqtop =
ctx#add_proposals (Option.get !self_provider) props true
method populate ctx =
- let iter = ctx#iter in
+ let iter = buffer#get_iter_at_mark `INSERT in
+ let () = insert_offset <- iter#offset in
+ let () = Minilib.log (Printf.sprintf "Completion at offset: %i" insert_offset) in
let buffer = new GText.buffer iter#buffer in
+ if not (Gtk_parsing.ends_word iter#backward_char) then self#add_proposals ctx Proposals.empty else
let start = Gtk_parsing.find_word_start iter in
+ if iter#offset - start#offset < auto_complete_length then self#add_proposals ctx Proposals.empty else
let w = start#get_text ~stop:iter in
let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in
let (off, prefix, props) = cache in
@@ -127,17 +131,7 @@ class completion_provider coqtop =
let occupied () = update synt in
Coq.try_grab coqtop query occupied
- method matched ctx =
- if !active then
- let iter = ctx#iter in
- let () = insert_offset <- iter#offset in
- let log = Printf.sprintf "Completion at offset: %i" insert_offset in
- let () = Minilib.log log in
- if Gtk_parsing.ends_word iter#backward_char then
- let start = Gtk_parsing.find_word_start iter in
- iter#offset - start#offset >= auto_complete_length
- else false
- else false
+ method matched ctx = !active
method activation = [`INTERACTIVE; `USER_REQUESTED]
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index 93c4cbb602..8bb34fbbca 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -10,7 +10,7 @@
module Proposals : sig type t end
-class completion_provider : Coq.coqtop ->
+class completion_provider : GText.buffer -> Coq.coqtop ->
object
inherit GSourceView3.source_completion_provider
method active : bool
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
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index f2d9f33d7d..62d58a5f23 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,7 +287,7 @@ end
class script_view (tv : source_view) (ct : Coq.coqtop) =
let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
-let provider = new Wg_Completion.completion_provider ct in
+let provider = new Wg_Completion.completion_provider view#buffer ct in
object (self)
inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:20:19 +0000