diff options
| -rw-r--r-- | ide/coq.ml | 1 | ||||
| -rw-r--r-- | ide/coq.mli | 1 | ||||
| -rw-r--r-- | ide/coqide.ml | 10 | ||||
| -rw-r--r-- | ide/ide.mllib | 2 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 26 | ||||
| -rw-r--r-- | ide/wg_ScriptView.mli | 50 | ||||
| -rw-r--r-- | lib/serialize.ml | 1 | ||||
| -rw-r--r-- | lib/serialize.mli | 3 |
8 files changed, 57 insertions, 37 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 1ce9379d2..d46a98738 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -327,6 +327,7 @@ let inloadpath coqtop s = eval_call coqtop (Serialize.inloadpath s) let mkcases coqtop s = eval_call coqtop (Serialize.mkcases s) let status coqtop = eval_call coqtop Serialize.status let hints coqtop = eval_call coqtop Serialize.hints +let search coqtop flags = eval_call coqtop (Serialize.search flags) let unsafe_close coqtop = if Mutex.try_lock coqtop.lock then begin diff --git a/ide/coq.mli b/ide/coq.mli index 454610b9b..a0f5c30f8 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -94,6 +94,7 @@ val evars : handle -> Interface.evar list option Interface.value val hints : handle -> (Interface.hint list * Interface.hint) option Interface.value val inloadpath : handle -> string -> bool Interface.value val mkcases : handle -> string -> string list list Interface.value +val search : handle -> Interface.search_flags -> Interface.search_answer list Interface.value (** A specialized version of [raw_interp] dedicated to set/unset options. *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 3549ee10f..de4474c16 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1199,11 +1199,6 @@ let create_session file = ?style_scheme:(style_manager#style_scheme current.source_style) () in - let script = - Wg_ScriptView.script_view - ~source_buffer:script_buffer - ~show_line_numbers:true - ~wrap_mode:`NONE () in let proof = GText.view ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ()) @@ -1227,6 +1222,11 @@ let create_session file = let reset = ref (fun _ -> ()) in let trigger handle = !reset handle in let ct = Coq.spawn_coqtop trigger coqtop_args in + let script = + Wg_ScriptView.script_view ct + ~source_buffer:script_buffer + ~show_line_numbers:true + ~wrap_mode:`NONE () in let command = new Wg_Command.command_window ct in let finder = new Wg_Find.finder (script :> GText.view) in let legacy_av = new analyzed_view script proof message ct file in diff --git a/ide/ide.mllib b/ide/ide.mllib index 3d8b82bdd..1ad52d4a4 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -16,11 +16,11 @@ Utf8_convert Preferences Project_file Ideutils +Coq Gtk_parsing Ideproof Wg_ScriptView Coq_lex -Coq Coq_commands Wg_Command Coqide_ui diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index cbc8212e9..8c679e4c1 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -42,7 +42,7 @@ end module Proposals = Set.Make(StringOrd) -let get_completion (buffer : GText.buffer) w = +let get_completion (buffer : GText.buffer) coqtop w = let rec get_aux accu (iter : GText.iter) = match iter#forward_search w with | None -> accu @@ -55,9 +55,23 @@ let get_completion (buffer : GText.buffer) w = get_aux (Proposals.add proposal accu) stop else get_aux accu stop in - get_aux Proposals.empty buffer#start_iter + let get_semantic accu = + let ans = ref accu in + let flags = [Interface.Name_Pattern ("^" ^ w), true] in + let query handle = match Coq.search handle flags with + | Interface.Good l -> + let fold accu elt = + Proposals.add elt.Interface.search_answer_base_name accu + in + ans := (List.fold_left fold accu l) + | _ -> () + in + Coq.try_grab coqtop query ignore; + !ans + in + get_semantic (get_aux Proposals.empty buffer#start_iter) -class script_view (tv : source_view) = +class script_view (tv : source_view) (ct : Coq.coqtop) = object (self) inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super @@ -175,7 +189,7 @@ object (self) if (start#offset = off) && (0 <= is_substring prefix w) then Proposals.filter (fun p -> 0 < is_substring w p) proposals else - let ans = get_completion self#buffer w in + let ans = get_completion self#buffer ct w in let () = last_completion <- (start#offset, w, ans) in ans in @@ -215,7 +229,7 @@ object (self) end -let script_view ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces = +let script_view ct ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces = GtkSourceView2.SourceView.make_params [] ~cont:( GtkText.View.make_params ~cont:( GContainer.pack_container ~create: @@ -226,4 +240,4 @@ let script_view ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces let w = Gobject.unsafe_cast w in Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl; Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces; - ((new script_view w) : script_view)))) + ((new script_view w ct) : script_view)))) diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index a2024eeec..b229eacfe 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -10,7 +10,7 @@ type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj -class script_view : source_view -> +class script_view : source_view -> Coq.coqtop -> object inherit GSourceView2.source_view method undo : unit -> bool @@ -20,27 +20,27 @@ object method set_auto_complete : bool -> unit end -val script_view : - ?source_buffer:GSourceView2.source_buffer -> - ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list -> - ?auto_indent:bool -> - ?highlight_current_line:bool -> - ?indent_on_tab:bool -> - ?indent_width:int -> - ?insert_spaces_instead_of_tabs:bool -> - ?right_margin_position:int -> - ?show_line_marks:bool -> - ?show_line_numbers:bool -> - ?show_right_margin:bool -> - ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> - ?tab_width:int -> - ?editable:bool -> - ?cursor_visible:bool -> - ?justification:GtkEnums.justification -> - ?wrap_mode:GtkEnums.wrap_mode -> - ?accepts_tab:bool -> - ?border_width:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> unit -> script_view +val script_view : Coq.coqtop -> + ?source_buffer:GSourceView2.source_buffer -> + ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list -> + ?auto_indent:bool -> + ?highlight_current_line:bool -> + ?indent_on_tab:bool -> + ?indent_width:int -> + ?insert_spaces_instead_of_tabs:bool -> + ?right_margin_position:int -> + ?show_line_marks:bool -> + ?show_line_numbers:bool -> + ?show_right_margin:bool -> + ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> + ?tab_width:int -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?accepts_tab:bool -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> unit -> script_view diff --git a/lib/serialize.ml b/lib/serialize.ml index 105775bda..fd1c6d055 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -69,6 +69,7 @@ let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s let mkcases s : string list list call = MkCases s +let search flags : search_answer list call = Search flags let quit : unit call = Quit (** * Coq answers to CoqIde *) diff --git a/lib/serialize.mli b/lib/serialize.mli index 357b8815b..0a1e9a107 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -58,6 +58,9 @@ val mkcases : string -> string list list call proof is in progress. *) val evars : evar list option call +(** Search for objects satisfying the given search flags. *) +val search : search_flags -> search_answer list call + (** Retrieve the list of options of the current toplevel, together with their state. *) val get_options : (option_name * option_state) list call |