aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq_commands.ml195
-rw-r--r--ide/coq_commands.mli1
-rw-r--r--ide/coqide.ml15
-rw-r--r--ide/coqide_ui.ml5
-rw-r--r--ide/idetop.ml1
-rw-r--r--ide/preferences.ml29
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/protocol/interface.ml2
-rw-r--r--ide/protocol/xmlprotocol.ml10
-rw-r--r--ide/wg_Completion.ml408
-rw-r--r--ide/wg_Completion.mli22
-rw-r--r--ide/wg_ScriptView.ml14
-rw-r--r--ide/wg_ScriptView.mli2
13 files changed, 101 insertions, 605 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index bfd99e7ce3..5b9ea17ba7 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -228,198 +228,3 @@ let state_preserving = [
"Test Printing Wildcard";
]
-
-
-let tactics =
- [
- [
- "abstract";
- "absurd";
- "apply";
- "apply __ with";
- "assert";
- "assert (__:__)";
- "assert (__:=__)";
- "assumption";
- "auto";
- "auto with";
- "autorewrite";
- ];
-
- [
- "case";
- "case __ with";
- "casetype";
- "cbv";
- "cbv in";
- "change";
- "change __ in";
- "clear";
- "clearbody";
- "cofix";
- "compare";
- "compute";
- "compute in";
- "congruence";
- "constructor";
- "constructor __ with";
- "contradiction";
- "cut";
- "cutrewrite";
- ];
-
- [
- "decide equality";
- "decompose";
- "decompose record";
- "decompose sum";
- "dependent inversion";
- "dependent inversion __ with";
- "dependent inversion__clear";
- "dependent inversion__clear __ with";
- "dependent rewrite ->";
- "dependent rewrite <-";
- "destruct";
- "discriminate";
- "do";
- "double induction";
- ];
-
- [
- "eapply";
- "eauto";
- "eauto with";
- "eexact";
- "elim";
- "elim __ using";
- "elim __ with";
- "elimtype";
- "exact";
- "exists";
- ];
-
- [
- "fail";
- "field";
- "first";
- "firstorder";
- "firstorder using";
- "firstorder with";
- "fix";
- "fix __ with";
- "fold";
- "fold __ in";
- "functional induction";
- ];
-
- [
- "generalize";
- "generalize dependent";
- ];
-
- [
- "hnf";
- ];
-
- [
- "idtac";
- "induction";
- "info";
- "injection";
- "instantiate (__:=__)";
- "intro";
- "intro after";
- "intro __ after";
- "intros";
- "intros until";
- "intuition";
- "inversion";
- "inversion __ in";
- "inversion __ using";
- "inversion __ using __ in";
- "inversion__clear";
- "inversion__clear __ in";
- ];
-
- [
- "jp <n>";
- "jp";
- ];
-
- [
- "lapply";
- "lazy";
- "lazy in";
- "left";
- ];
-
- [
- "move __ after";
- ];
-
- [
- "omega";
- ];
-
- [
- "pattern";
- "pose";
- "pose __:=__)";
- "progress";
- ];
-
- [
- "quote";
- ];
-
- [
- "red";
- "red in";
- "refine";
- "reflexivity";
- "rename __ into";
- "repeat";
- "replace __ with";
- "rewrite";
- "rewrite __ in";
- "rewrite <-";
- "rewrite <- __ in";
- "right";
- "ring";
- ];
-
- [
- "set";
- "set (__:=__)";
- "setoid__replace";
- "setoid__rewrite";
- "simpl";
- "simpl __ in";
- "simple destruct";
- "simple induction";
- "simple inversion";
- "simplify__eq";
- "solve";
- "split";
-(* "split__Rabs";
- "split__Rmult";
-*)
- "subst";
- "symmetry";
- "symmetry in";
- ];
-
- [
- "tauto";
- "transitivity";
- "trivial";
- "try";
- ];
-
- [
- "unfold";
- "unfold __ in";
- ];
-]
-
-
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
index 5f8ce30901..c8c11f77af 100644
--- a/ide/coq_commands.mli
+++ b/ide/coq_commands.mli
@@ -8,6 +8,5 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val tactics : string list list
val commands : string list list
val state_preserving : string list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fc30690544..ccf6d40b2b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -618,7 +618,7 @@ let printopts_callback opts v =
let get_current_word term =
(* First look to find if autocompleting *)
- match term.script#complete_popup#proposal with
+ match term.script#proposal with
| Some p -> p
| None ->
(* Then look at the current selected word *)
@@ -977,7 +977,6 @@ let build_ui () =
let view_menu = GAction.action_group ~name:"View" () in
let export_menu = GAction.action_group ~name:"Export" () in
let navigation_menu = GAction.action_group ~name:"Navigation" () in
- let tactics_menu = GAction.action_group ~name:"Tactics" () in
let templates_menu = GAction.action_group ~name:"Templates" () in
let tools_menu = GAction.action_group ~name:"Tools" () in
let queries_menu = GAction.action_group ~name:"Queries" () in
@@ -985,7 +984,7 @@ let build_ui () =
let windows_menu = GAction.action_group ~name:"Windows" () in
let help_menu = GAction.action_group ~name:"Help" () in
let all_menus = [
- file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu;
+ file_menu; edit_menu; view_menu; export_menu; navigation_menu;
templates_menu; tools_menu; queries_menu; compile_menu; windows_menu;
help_menu; ] in
@@ -996,8 +995,6 @@ let build_ui () =
item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
- item "Revert all buffers" ~label:"_Revert all buffers"
- ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED;
item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer";
item "Print..." ~label:"_Print..."
@@ -1121,11 +1118,6 @@ let build_ui () =
("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
] end;
- menu tactics_menu [
- item "Tactics" ~label:"_Tactics";
- ];
- alpha_items tactics_menu "Tactic" Coq_commands.tactics;
-
menu templates_menu [
item "Templates" ~label:"Te_mplates";
template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
@@ -1209,7 +1201,6 @@ let build_ui () =
Coqide_ui.ui_m#insert_action_group edit_menu 0;
Coqide_ui.ui_m#insert_action_group view_menu 0;
Coqide_ui.ui_m#insert_action_group navigation_menu 0;
- Coqide_ui.ui_m#insert_action_group tactics_menu 0;
Coqide_ui.ui_m#insert_action_group templates_menu 0;
Coqide_ui.ui_m#insert_action_group tools_menu 0;
Coqide_ui.ui_m#insert_action_group queries_menu 0;
@@ -1368,7 +1359,7 @@ let read_coqide_args argv =
|"-debug"::args ->
Minilib.debug := true;
Flags.debug := true;
- Backtrace.record_backtrace true;
+ Exninfo.record_backtrace true;
filter_coqtop coqtop project_files bindings_files ("-debug"::out) args
|"-coqtop-flags" :: flags :: args->
Coq.ideslave_coqtop_flags := Some flags;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index f056af6703..f22821c6ea 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -36,7 +36,6 @@ let init () =
\n <menuitem action='Save' />\
\n <menuitem action='Save as' />\
\n <menuitem action='Save all' />\
-\n <menuitem action='Revert all buffers' />\
\n <menuitem action='Close buffer' />\
\n <menuitem action='Print...' />\
\n <menu action='Export to'>\
@@ -100,9 +99,6 @@ let init () =
\n <menuitem action='Previous' />\
\n <menuitem action='Next' />\
\n </menu>\
-\n <menu action='Tactics'>\
-\n %s\
-\n </menu>\
\n <menu action='Templates'>\
\n <menuitem action='Lemma' />\
\n <menuitem action='Theorem' />\
@@ -165,7 +161,6 @@ let init () =
\n</toolbar>\
\n</ui>"
(if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
- (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
(Buffer.contents (list_items "Template" Coq_commands.commands))
(Buffer.contents (list_queries "User-Query" Preferences.user_queries#get))
in
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7d92cff365..ae2301a0a7 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -360,7 +360,6 @@ let import_option_value = function
let export_option_state s = {
Interface.opt_sync = true;
Interface.opt_depr = s.Goptions.opt_depr;
- Interface.opt_name = s.Goptions.opt_name;
Interface.opt_value = export_option_value s.Goptions.opt_value;
}
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4ee5669877..af1759b0bb 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -331,10 +331,6 @@ let modifier_for_navigation =
let modifier_for_templates =
new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
-let modifier_for_tactics =
- new preference ~name:["modifier_for_tactics"]
- ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string)
-
let modifier_for_display =
new preference ~name:["modifier_for_display"]
~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
@@ -347,7 +343,6 @@ let attach_modifiers_callback () =
(* To be done after the preferences are loaded *)
let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in
let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in
- let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in
let _ = attach_modifiers modifier_for_display "<Actions>/View/" in
let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in
()
@@ -388,6 +383,9 @@ let window_height =
let auto_complete =
new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool)
+let auto_complete_delay =
+ new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int)
+
let stop_before =
new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool)
@@ -831,10 +829,26 @@ let configure ?(apply=(fun () -> ())) parent =
let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
in
+ let spin text ~min ~max (pref : int preference) =
+ let box = GPack.hbox ~packing:box#pack () in
+ let but = GEdit.spin_button
+ ~numeric:true ~update_policy:`IF_VALID ~digits:0
+ ~packing:box#pack ()
+ in
+ let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in
+ let () = but#adjustment#set_bounds
+ ~lower:(float_of_int min) ~upper:(float_of_int max)
+ ~step_incr:1.
+ ()
+ in
+ let () = but#set_value (float_of_int pref#get) in
+ ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int))
+ in
let () = button "Dynamic word wrap" dynamic_word_wrap in
let () = button "Show line number" show_line_number in
let () = button "Auto indentation" auto_indent in
let () = button "Auto completion" auto_complete in
+ let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in
let () = button "Show spaces" show_spaces in
let () = button "Show right margin" show_right_margin in
let () = button "Show progress bar" show_progress_bar in
@@ -932,9 +946,6 @@ let configure ?(apply=(fun () -> ())) parent =
(string_of_project_behavior read_project#get)
in
let project_file_name = pstring "Default name for project file" project_file_name in
- let modifier_for_tactics =
- pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics
- in
let modifier_for_templates =
pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates
in
@@ -1037,7 +1048,7 @@ let configure ?(apply=(fun () -> ())) parent =
[cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
cmd_print;cmd_editor;cmd_browse]);
Section("Shortcuts", Some `PREFERENCES,
- [modifiers_valid; modifier_for_tactics;
+ [modifiers_valid;
modifier_for_templates; modifier_for_display; modifier_for_navigation;
modifier_for_queries (*; user_queries *)]);
Section("Misc", Some `ADD,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 4b04326cec..754f15c575 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,7 +71,6 @@ val automatic_tactics : string list preference
val cmd_print : string preference
val modifier_for_navigation : string preference
val modifier_for_templates : string preference
-val modifier_for_tactics : string preference
val modifier_for_display : string preference
val modifier_for_queries : string preference
val modifiers_valid : string preference
@@ -82,6 +81,7 @@ val show_toolbar : bool preference
val window_width : int preference
val window_height : int preference
val auto_complete : bool preference
+val auto_complete_delay : int preference
val stop_before : bool preference
val reset_on_tab_switch : bool preference
val line_ending : line_ending preference
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..be5e305ad3 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -71,8 +71,6 @@ type option_state = {
(** Whether an option is synchronous *)
opt_depr : bool;
(** Whether an option is deprecated *)
- opt_name : string;
- (** A short string that is displayed when using [Test] *)
opt_value : option_value;
(** The current value of the option *)
}
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index cad65cc5d6..a2c80ea118 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -79,13 +79,11 @@ let of_option_state s =
Element ("option_state", [], [
of_bool s.opt_sync;
of_bool s.opt_depr;
- of_string s.opt_name;
of_option_value s.opt_value])
let to_option_state = function
- | Element ("option_state", [], [sync; depr; name; value]) -> {
+ | Element ("option_state", [], [sync; depr; value]) -> {
opt_sync = to_bool sync;
opt_depr = to_bool depr;
- opt_name = to_string name;
opt_value = to_option_value value }
| x -> raise (Marshal_error("option_state",x))
@@ -429,8 +427,8 @@ end = struct
| StringOptValue (Some s) -> s
| BoolValue b -> if b then "true" else "false"
let pr_option_state (s : option_state) =
- Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
- s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+ Printf.sprintf "sync := %b; depr := %b; value := %s\n"
+ s.opt_sync s.opt_depr (pr_option_value s.opt_value)
let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
let pr_coq_object (o : 'a coq_object) = "FIXME"
@@ -513,7 +511,7 @@ end = struct
"type which contains a flattened n-tuple. We provide one example.\n");
Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
(pr_xml (of_option_state { opt_sync = true; opt_depr = false;
- opt_name = "name1"; opt_value = IntValue (Some 37) }));
+ opt_value = IntValue (Some 37) }));
end
open ReifType
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index ac6712909e..396939cfcc 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -69,387 +69,101 @@ let is_substring s1 s2 =
if !break then len2 - len1
else -1
-class type complete_model_signals =
- object ('a)
- method after : 'a
- method disconnect : GtkSignal.id -> unit
- method start_completion : callback:(int -> unit) -> GtkSignal.id
- method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id
- method end_completion : callback:(unit -> unit) -> GtkSignal.id
- end
-
-let complete_model_signals
- (start_s : int GUtil.signal)
- (update_s : (int * string * Proposals.t) GUtil.signal)
- (end_s : unit GUtil.signal) : complete_model_signals =
-let signals = [
- start_s#disconnect;
- update_s#disconnect;
- end_s#disconnect;
-] in
-object (self : 'a)
- inherit GUtil.ml_signals signals
- method start_completion = start_s#connect ~after
- method update_completion = update_s#connect ~after
- method end_completion = end_s#connect ~after
-end
-
-class complete_model coqtop (buffer : GText.buffer) =
- let cols = new GTree.column_list in
- let column = cols#add Gobject.Data.string in
- let store = GTree.list_store cols in
- let filtered_store = GTree.model_filter store in
- let start_completion_signal = new GUtil.signal () in
- let update_completion_signal = new GUtil.signal () in
- let end_completion_signal = new GUtil.signal () in
-object (self)
-
- val signals = complete_model_signals
- start_completion_signal update_completion_signal end_completion_signal
- val mutable active = false
- val mutable auto_complete_length = 3
- (* this variable prevents CoqIDE from autocompleting when we have deleted something *)
- val mutable is_auto_completing = false
- (* this mutex ensure that CoqIDE will not try to autocomplete twice *)
- val mutable cache = (-1, "", Proposals.empty)
- val mutable insert_offset = -1
- val mutable current_completion = ("", Proposals.empty)
- val mutable lock_auto_completing = true
+class completion_provider coqtop =
+ let self_provider = ref None in
+ let active = ref true in
+ let provider = object (self)
- method connect = signals
+ val mutable auto_complete_length = 3
+ val mutable cache = (-1, "", Proposals.empty)
+ val mutable insert_offset = -1
- method active = active
+ method name = ""
- method set_active b = active <- b
+ method icon = None
- method private handle_insert iter s =
- (* we're inserting, so we may autocomplete *)
- is_auto_completing <- true
+ method private update_proposals pref =
+ let (_, _, props) = cache in
+ let filter prop = 0 <= is_substring pref prop in
+ let props = Proposals.filter filter props in
+ props
- method private handle_delete ~start ~stop =
- (* disable autocomplete *)
- is_auto_completing <- false
-
- method store = filtered_store
-
- method column = column
-
- method handle_proposal path =
- let row = filtered_store#get_iter path in
- let proposal = filtered_store#get ~row ~column in
- let (start_offset, _, _) = cache in
- (* [iter] might be invalid now, get a new one to please gtk *)
- let iter = buffer#get_iter `INSERT in
- (* We cancel completion when the buffer has changed recently *)
- if iter#offset = insert_offset then begin
- let suffix =
- let len1 = String.length proposal in
- let len2 = insert_offset - start_offset in
- String.sub proposal len2 (len1 - len2)
+ method private add_proposals ctx props =
+ let mk text =
+ let item = GSourceView3.source_completion_item ~text ~label:text () in
+ (item :> GSourceView3.source_completion_proposal)
in
- buffer#begin_user_action ();
- ignore (buffer#insert_interactive ~iter suffix);
- buffer#end_user_action ();
- end
-
- method private init_proposals pref props =
- let () = store#clear () in
- let iter prop =
- let iter = store#append () in
- store#set ~row:iter ~column prop
- in
- let () = current_completion <- (pref, props) in
- Proposals.iter iter props
-
- method private update_proposals pref =
- let (_, _, props) = cache in
- let filter prop = 0 <= is_substring pref prop in
- let props = Proposals.filter filter props in
- let () = current_completion <- (pref, props) in
- let () = filtered_store#refilter () in
- props
-
- method private do_auto_complete k =
- let iter = buffer#get_iter `INSERT in
- let () = insert_offset <- iter#offset in
- let log = Printf.sprintf "Completion at offset: %i" insert_offset in
- let () = Minilib.log log in
- let prefix =
- if Gtk_parsing.ends_word iter then
- let start = Gtk_parsing.find_word_start iter in
- let w = buffer#get_text ~start ~stop:iter () in
- if String.length w >= auto_complete_length then Some (w, start)
- else None
- else None
- in
- match prefix with
- | Some (w, start) ->
+ let props = List.map mk (Proposals.elements props) in
+ ctx#add_proposals (Option.get !self_provider) props true
+
+ method populate ctx =
+ let iter = ctx#iter in
+ let buffer = new GText.buffer iter#buffer in
+ let start = Gtk_parsing.find_word_start iter in
+ let w = start#get_text ~stop:iter in
let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in
let (off, prefix, props) = cache in
let start_offset = start#offset in
(* check whether we have the last request in cache *)
if (start_offset = off) && (0 <= is_substring prefix w) then
let props = self#update_proposals w in
- let () = update_completion_signal#call (start_offset, w, props) in
- k ()
+ self#add_proposals ctx props
else
- let () = start_completion_signal#call start_offset in
+ let cancel = ref false in
+ let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in
let update props =
let () = cache <- (start_offset, w, props) in
- let () = self#init_proposals w props in
- update_completion_signal#call (start_offset, w, props)
+ if not !cancel then self#add_proposals ctx props
in
(* If not in the cache, we recompute it: first syntactic *)
let synt = get_syntactic_completion buffer w Proposals.empty in
(* Then semantic *)
- let next prop =
- let () = update prop in
- Coq.lift k
+ let next props =
+ update props;
+ Coq.return ()
in
let query = Coq.bind (get_semantic_completion w synt) next in
(* If coqtop is computing, do the syntactic completion altogether *)
- let occupied () =
- let () = update synt in
- k ()
- in
+ let occupied () = update synt in
Coq.try_grab coqtop query occupied
- | None -> end_completion_signal#call (); k ()
-
- method private may_auto_complete () =
- if active && is_auto_completing && lock_auto_completing then begin
- let () = lock_auto_completing <- false in
- let unlock () = lock_auto_completing <- true in
- self#do_auto_complete unlock
- end
-
- initializer
- let filter_prop model row =
- let (_, props) = current_completion in
- let prop = store#get ~row ~column in
- Proposals.mem prop props
- in
- let () = filtered_store#set_visible_func filter_prop in
- (* Install auto-completion *)
- ignore (buffer#connect#insert_text ~callback:self#handle_insert);
- ignore (buffer#connect#delete_range ~callback:self#handle_delete);
- ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete);
-
-end
-
-class complete_popup (model : complete_model) (view : GText.view) =
- let obj = GWindow.window ~kind:`POPUP ~show:false () in
- let frame = GBin.scrolled_window
- ~hpolicy:`NEVER ~vpolicy:`NEVER
- ~shadow_type:`OUT ~packing:obj#add ()
- in
-(* let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *)
- let data = GTree.view
- ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment
- ~rules_hint:true ~headers_visible:false
- ~model:model#store ~packing:frame#add ()
- in
- let renderer = GTree.cell_renderer_text [], ["text", model#column] in
- let col = GTree.view_column ~renderer () in
- let _ = data#append_column col in
- let () = col#set_sizing `AUTOSIZE in
- let page_size = 16 in
-
-object (self)
-
- method coerce = view#coerce
-
- method private refresh_style () =
- let (renderer, _) = renderer in
- let font = Pango.Font.from_string Preferences.text_font#get in
- renderer#set_properties [`FONT_DESC font; `XPAD 10]
-
- method private coordinates pos =
- (* Toplevel position w.r.t. screen *)
- let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in
- (* Position of view w.r.t. window *)
- let (ux, uy) = Gdk.Window.get_position view#misc#window in
- (* Relative buffer position to view *)
- let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
- (* Iter position *)
- let iter = view#buffer#get_iter pos in
- let coords = view#get_iter_location iter in
- let lx = Gdk.Rectangle.x coords in
- let ly = Gdk.Rectangle.y coords in
- let w = Gdk.Rectangle.width coords in
- let h = Gdk.Rectangle.height coords in
- (* Absolute position *)
- (x + lx + ux - dx, y + ly + uy - dy, w, h)
-
- method private select_any f =
- let sel = data#selection#get_selected_rows in
- let path = match sel with
- | [] ->
- begin match model#store#get_iter_first with
- | None -> None
- | Some iter -> Some (model#store#get_path iter)
- end
- | path :: _ -> Some path
- in
- match path with
- | None -> ()
- | Some path ->
- let path = f path in
- let _ = data#selection#select_path path in
- data#scroll_to_cell ~align:(0.,0.) path col
-
- method private select_previous () =
- let prev path =
- let copy = GTree.Path.copy path in
- if GTree.Path.prev path then path
- else copy
- in
- self#select_any prev
-
- method private select_next () =
- let next path =
- let () = GTree.Path.next path in
- path
- in
- self#select_any next
- method private select_previous_page () =
- let rec up i path =
- if i = 0 then path
- else
- let copy = GTree.Path.copy path in
- let has_prev = GTree.Path.prev path in
- if has_prev then up (pred i) path
- else copy
- in
- self#select_any (up page_size)
+ 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 private select_next_page () =
- let rec down i path =
- if i = 0 then path
- else
- let copy = GTree.Path.copy path in
- let iter = model#store#get_iter path in
- let has_next = model#store#iter_next iter in
- if has_next then down (pred i) (model#store#get_path iter)
- else copy
- in
- self#select_any (down page_size)
+ method activation = [`INTERACTIVE; `USER_REQUESTED]
- method private select_first () =
- let rec up path =
- let copy = GTree.Path.copy path in
- let has_prev = GTree.Path.prev path in
- if has_prev then up path
- else copy
- in
- self#select_any up
+ method info_widget proposal = None
- method private select_last () =
- let rec down path =
- let copy = GTree.Path.copy path in
- let iter = model#store#get_iter path in
- let has_next = model#store#iter_next iter in
- if has_next then down (model#store#get_path iter)
- else copy
- in
- self#select_any down
+ method update_info proposal info = ()
- method private select_enter () =
- let sel = data#selection#get_selected_rows in
- match sel with
- | [] -> ()
- | path :: _ ->
- let () = model#handle_proposal path in
- self#hide ()
+ method start_iter ctx proposal iter = false
- method proposal =
- let sel = data#selection#get_selected_rows in
- if obj#misc#visible then match sel with
- | [] -> None
- | path :: _ ->
- let row = model#store#get_iter path in
- let column = model#column in
- let proposal = model#store#get ~row ~column in
- Some proposal
- else None
+ method activate_proposal proposal iter = false
- method private manage_scrollbar () =
- (* HACK: we don't have access to the treeview size because of the lack of
- LablGTK binding for certain functions, so we bypass it by approximating
- it through the size of the proposals *)
- let height = match model#store#get_iter_first with
- | None -> -1
- | Some iter ->
- let path = model#store#get_path iter in
- let area = data#get_cell_area ~path ~col () in
- let height = Gdk.Rectangle.height area in
- let height = page_size * height in
- height
- in
- let len = ref 0 in
- let () = model#store#foreach (fun _ _ -> incr len; false) in
- if !len > page_size then
- let () = frame#set_vpolicy `ALWAYS in
- data#misc#set_size_request ~height ()
- else
- data#misc#set_size_request ~height:(-1) ()
+ method interactive_delay = (-1)
- method private refresh () =
- let () = frame#set_vpolicy `NEVER in
- let () = self#select_first () in
- let () = obj#misc#show () in
- let () = self#manage_scrollbar () in
- obj#resize ~width:1 ~height:1
+ method priority = 0
- method private start_callback off =
- let (x, y, w, h) = self#coordinates (`OFFSET off) in
- let () = obj#move ~x ~y:(y + 3 * h / 2) in
- ()
+ end in
+ let provider = GSourceView3.source_completion_provider provider in
+ object (self)
- method private update_callback (off, word, props) =
- if Proposals.is_empty props then self#hide ()
- else if Proposals.mem word props then self#hide ()
- else self#refresh ()
+ inherit GSourceView3.source_completion_provider provider#as_source_completion_provider
- method private end_callback () =
- obj#misc#hide ()
+ method active = !active
- method private hide () = self#end_callback ()
+ method set_active b = active := b
- initializer
- let move_cb _ _ ~extend = self#hide () in
- let key_cb ev =
- let eval cb = cb (); true in
- let ev_key = GdkEvent.Key.keyval ev in
- if obj#misc#visible then
- if ev_key = GdkKeysyms._Up then eval self#select_previous
- else if ev_key = GdkKeysyms._Down then eval self#select_next
- else if ev_key = GdkKeysyms._Tab then eval self#select_enter
- else if ev_key = GdkKeysyms._Return then eval self#select_enter
- else if ev_key = GdkKeysyms._Escape then eval self#hide
- else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page
- else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page
- else if ev_key = GdkKeysyms._Home then eval self#select_first
- else if ev_key = GdkKeysyms._End then eval self#select_last
- else false
- else false
- in
- (* Style handling *)
- let _ = view#misc#connect#style_set ~callback:self#refresh_style in
- let _ = self#refresh_style () in
- let _ = data#set_resize_mode `PARENT in
- let _ = frame#set_resize_mode `PARENT in
- (* Callback to model *)
- let _ = model#connect#start_completion ~callback:self#start_callback in
- let _ = model#connect#update_completion ~callback:self#update_callback in
- let _ = model#connect#end_completion ~callback:self#end_callback in
- (* Popup interaction *)
- let _ = view#event#connect#key_press ~callback:key_cb in
- (* Hiding the popup when necessary*)
- let _ = view#misc#connect#hide ~callback:obj#misc#hide in
- let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in
- let _ = view#connect#move_cursor ~callback:move_cb in
- let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in
- ()
+ initializer
+ self_provider := Some (self :> GSourceView3.source_completion_provider)
-end
+ end
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index ac9e6cd94f..020fe26cfb 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -10,27 +10,9 @@
module Proposals : sig type t end
-class type complete_model_signals =
- object ('a)
- method after : 'a
- method disconnect : GtkSignal.id -> unit
- method start_completion : callback:(int -> unit) -> GtkSignal.id
- method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id
- method end_completion : callback:(unit -> unit) -> GtkSignal.id
- end
-
-class complete_model : Coq.coqtop -> GText.buffer ->
+class completion_provider : Coq.coqtop ->
object
+ inherit GSourceView3.source_completion_provider
method active : bool
- method connect : complete_model_signals
method set_active : bool -> unit
- method store : GTree.model_filter
- method column : string GTree.column
- method handle_proposal : Gtk.tree_path -> unit
-end
-
-class complete_popup : complete_model -> GText.view ->
-object
- method coerce : GObj.widget
- method proposal : string option
end
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 769ce61ee1..b7a35d7e94 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,18 +287,17 @@ end
class script_view (tv : source_view) (ct : Coq.coqtop) =
let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
-let completion = new Wg_Completion.complete_model ct view#buffer in
-let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
+let provider = new Wg_Completion.completion_provider ct in
object (self)
inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
val undo_manager = new undo_manager view#buffer
- method auto_complete = completion#active
+ method auto_complete = provider#active
method set_auto_complete flag =
- completion#set_active flag
+ provider#set_active flag
method recenter_insert =
self#scroll_to_mark
@@ -448,7 +447,7 @@ object (self)
self#buffer#delete_mark (`MARK insert_mark)
- method complete_popup = popup
+ method proposal : string option = None (* FIXME *)
method undo = undo_manager#undo
method redo = undo_manager#redo
@@ -527,10 +526,15 @@ object (self)
stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs;
stick tab_length self self#set_tab_width;
stick auto_complete self self#set_auto_complete;
+ stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d);
let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font self cb;
+ let () = self#completion#set_accelerators 0 in
+ let () = self#completion#set_show_headers false in
+ let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in
+
()
end
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index 91c8e758a5..4b6591e063 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -28,7 +28,7 @@ object
method uncomment : unit -> unit
method apply_unicode_binding : unit -> unit
method recenter_insert : unit
- method complete_popup : Wg_Completion.complete_popup
+ method proposal : string option
end
val script_view : Coq.coqtop ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:25:33 +0000