diff options
| -rw-r--r-- | ide/coqide.ml | 163 | ||||
| -rw-r--r-- | ide/gtk_parsing.ml | 12 | ||||
| -rw-r--r-- | ide/ide.mllib | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 9 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 92 | ||||
| -rw-r--r-- | ide/wg_ScriptView.mli | 2 |
7 files changed, 125 insertions, 157 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index b5181b0f1..a67d42202 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -26,7 +26,6 @@ let safety_tag = function class type _analyzed_view = object - method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b method kill_detached_views : unit -> unit method add_detached_view : GWindow.window -> unit @@ -58,7 +57,6 @@ object method show_goals : unit method undo_last_step : unit method help_for_keyword : unit -> unit - method complete_at_offset : int -> bool end @@ -314,53 +312,6 @@ let setopts ct opts v = let opts = List.map (fun o -> (o, v)) opts in Coq.PrintOpt.set ct opts -(* Reset this to None on page change ! *) -let (last_completion:(string*int*int*bool) option ref) = ref None - -let () = to_do_on_page_switch := - (fun i -> last_completion := None)::!to_do_on_page_switch - -let rec complete input_buffer w (offset:int) = - match !last_completion with - | Some (lw,loffset,lpos,backward) - when lw=w && loffset=offset -> - begin - let iter = input_buffer#get_iter (`OFFSET lpos) in - if backward then - match complete_backward w iter with - | None -> - last_completion := - Some (lw,loffset, - (find_word_end - (input_buffer#get_iter (`OFFSET loffset)))#offset , - false); - None - | Some (ss,start,stop) as result -> - last_completion := - Some (w,offset,ss#offset,true); - result - else - match complete_forward w iter with - | None -> - last_completion := None; - None - | Some (ss,start,stop) as result -> - last_completion := - Some (w,offset,ss#offset,false); - result - end - | _ -> begin - match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with - | None -> - last_completion := - Some (w,offset,(find_word_end (input_buffer#get_iter - (`OFFSET offset)))#offset,false); - complete input_buffer w offset - | Some (ss,start,stop) as result -> - last_completion := Some (w,offset,ss#offset,true); - result - end - let get_current_word () = match session_notebook#current_term,cb#text with | {script=script; analyzed_view=av;},None -> @@ -376,7 +327,6 @@ let get_current_word () = prerr_endline t; t - let input_channel b ic = let buf = String.create 1024 and len = ref 0 in while len := input ic buf 0 1024; !len > 0 do @@ -532,18 +482,8 @@ object(self) val mutable last_auto_save_time = 0. val mutable detached_views = [] - val mutable auto_complete_on = current.auto_complete val hidden_proofs = Hashtbl.create 32 - method private toggle_auto_complete = - auto_complete_on <- not auto_complete_on - method private set_auto_complete t = auto_complete_on <- t - method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x -> - let old = auto_complete_on in - self#set_auto_complete false; - let y = f x in - self#set_auto_complete old; - y method add_detached_view (w:GWindow.window) = detached_views <- w::detached_views method remove_detached_view (w:GWindow.window) = @@ -850,30 +790,6 @@ object(self) else None with Not_found -> None - method complete_at_offset (offset:int) = - prerr_endline ("Completion at offset : " ^ string_of_int offset); - let it () = input_buffer#get_iter (`OFFSET offset) in - let iit = it () in - let start = find_word_start iit in - if ends_word iit then - let w = input_buffer#get_text - ~start - ~stop:iit - () - in - if String.length w <> 0 then begin - prerr_endline ("Completion of prefix : '" ^ w^"'"); - match complete input_buffer w start#offset with - | None -> false - | Some (ss,start,stop) -> - let completion = input_buffer#get_text ~start ~stop () in - ignore (input_buffer#delete_selection ()); - ignore (input_buffer#insert_interactive completion); - input_buffer#move_mark `SEL_BOUND ~where:(it())#backward_char; - true - end else false - else false - method private process_one_phrase ct verbosely display_goals do_highlight = let get_next_phrase () = self#clear_message; @@ -1273,21 +1189,6 @@ object(self) end ) ); - ignore (input_buffer#connect#after#insert_text - ~callback:(fun it s -> - if auto_complete_on && - String.length s = 1 && s <> " " && s <> "\n" - then - let v = session_notebook#current_term.analyzed_view - in - let has_completed = - v#complete_at_offset - ((input_view#buffer#get_iter `SEL_BOUND)#offset) - in - if has_completed then - input_buffer#move_mark `SEL_BOUND ~where:(input_buffer#get_iter `SEL_BOUND)#forward_char; - ) - ); ignore (input_buffer#connect#begin_user_action ~callback:(fun () -> let here = input_buffer#get_iter_at_mark `INSERT in @@ -1428,14 +1329,6 @@ let create_session file = script#buffer#place_cursor ~where:(script#buffer#start_iter); proof#misc#set_can_focus true; message#misc#set_can_focus true; - (* setting fonts *) - script#misc#modify_font current.text_font; - proof#misc#modify_font current.text_font; - message#misc#modify_font current.text_font; - (* setting colors *) - script#misc#modify_base [`NORMAL, `NAME current.background_color]; - proof#misc#modify_base [`NORMAL, `NAME current.background_color]; - message#misc#modify_base [`NORMAL, `NAME current.background_color]; { tab_label=basename; script=script; @@ -1639,7 +1532,8 @@ let load_file handler f = input_buffer#set_modified false; prerr_endline "Loading: clear undo"; session.script#clear_undo (); - prerr_endline "Loading: success" + prerr_endline "Loading: success"; + !refresh_editor_hook (); end with | e -> handler ("Load failed: "^(Printexc.to_string e)) @@ -1729,6 +1623,7 @@ let main files = let new_f _ = let session = create_session None in let index = session_notebook#append_term session in + !refresh_editor_hook (); session_notebook#goto_page index in let load_f _ = @@ -1835,19 +1730,7 @@ let main files = then current.proof_view#as_view else current.message_view#as_view in - (* - let toggle_auto_complete_i = - edit_f#add_check_item "_Auto Completion" - ~active:current.auto_complete - ~callback: - in - *) - (* - auto_complete := - (fun b -> match session_notebook#current_term.analyzed_view with - | Some av -> av#set_auto_complete b - | None -> ()); - *) + (* begin Preferences *) let reset_revert_timer () = disconnect_revert_timer (); @@ -2115,8 +1998,7 @@ let main files = GAction.add_action "Undo" ~accel:"<Ctrl>u" ~callback:(fun _ -> do_if_not_computing "undo" (fun sess -> - ignore (sess.analyzed_view#without_auto_complete - session_notebook#current_term.script#undo ())) + ignore (session_notebook#current_term.script#undo ())) [session_notebook#current_term]) ~stock:`UNDO; GAction.add_action "Redo" ~stock:`REDO ~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ())); @@ -2143,9 +2025,9 @@ let main files = GAction.add_action "Close Find" ~accel:"Escape" ~callback:(fun _ -> session_notebook#current_term.finder#hide ()); GAction.add_action "Complete Word" ~label:"Complete Word" ~callback:(fun _ -> - ignore ( - let av = session_notebook#current_term.analyzed_view in - av#complete_at_offset (av#get_insert)#offset + ignore ( () +(* let av = session_notebook#current_term.analyzed_view in + av#complete_at_offset (av#get_insert)#offset*) )) ~accel:"<Ctrl>slash"; GAction.add_action "External editor" ~label:"External editor" ~callback:(fun _ -> let av = session_notebook#current_term.analyzed_view in @@ -2381,37 +2263,35 @@ let main files = if current.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) else 0 in + let fd = current.text_font in + let clr = Tags.color_of_string current.background_color in + let iter_page p = + (* Editor settings *) p.script#set_wrap_mode wrap_mode; p.script#set_show_line_numbers current.show_line_number; p.script#set_auto_indent current.auto_indent; + (* Hack to handle missing binding in lablgtk *) let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int } in Gobject.set conv p.script#as_widget show_spaces; + p.script#set_insert_spaces_instead_of_tabs current.spaces_instead_of_tabs; p.script#set_tab_width current.tab_length; - in - List.iter iter_page session_notebook#pages; - ); - refresh_font_hook := - (fun () -> - let fd = current.text_font in - let iter_page p = + p.script#set_auto_complete current.auto_complete; + + (* Fonts *) p.script#misc#modify_font fd; p.proof_view#misc#modify_font fd; p.message_view#misc#modify_font fd; - p.command#refresh_font () - in - List.iter iter_page session_notebook#pages; - ); - refresh_background_color_hook := - (fun () -> - let clr = Tags.color_of_string current.background_color in - let iter_page p = + p.command#refresh_font (); + + (* Colors *) p.script#misc#modify_base [`NORMAL, `COLOR clr]; p.proof_view#misc#modify_base [`NORMAL, `COLOR clr]; p.message_view#misc#modify_base [`NORMAL, `COLOR clr]; p.command#refresh_color () + in List.iter iter_page session_notebook#pages; ); @@ -2511,6 +2391,7 @@ let main files = begin let session = create_session None in let index = session_notebook#append_term session in + !refresh_editor_hook (); session_notebook#goto_page index; end; initial_about session_notebook#current_term.proof_view#buffer; diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index c69f92e2d..590a3493f 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ideutils let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0) @@ -21,14 +22,12 @@ let is_word_char c = let starts_word (it:GText.iter) = - prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'"); - (not it#copy#nocopy#backward_char || - (let c = it#backward_char#char in - not (is_word_char c))) - + (it#is_start || + (let c = it#backward_char#char in + not (is_word_char c))) let ends_word (it:GText.iter) = - (not it#copy#nocopy#forward_char || + (it#is_end || let c = it#forward_char#char in not (is_word_char c) ) @@ -56,7 +55,6 @@ let find_word_start (it:GText.iter) = in step_to_start it#copy - let find_word_end (it:GText.iter) = let rec step_to_end (it:GText.iter) = prerr_endline "Find word end"; diff --git a/ide/ide.mllib b/ide/ide.mllib index c2df9bf47..3d8b82bdd 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -16,10 +16,10 @@ Utf8_convert Preferences Project_file Ideutils +Gtk_parsing Ideproof Wg_ScriptView Coq_lex -Gtk_parsing Coq Coq_commands Wg_Command diff --git a/ide/preferences.ml b/ide/preferences.ml index 24e93d0cd..6e18b4d34 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -74,12 +74,9 @@ let inputenc_of_string s = (** Hooks *) -let refresh_font_hook = ref (fun () -> ()) let refresh_style_hook = ref (fun () -> ()) let refresh_editor_hook = ref (fun () -> ()) -let refresh_background_color_hook = ref (fun () -> ()) let refresh_toolbar_hook = ref (fun () -> ()) -let auto_complete_hook = ref (fun x -> ()) let contextual_menus_on_goal_hook = ref (fun x -> ()) let resize_window_hook = ref (fun () -> ()) let refresh_tabs_hook = ref (fun () -> ()) @@ -410,7 +407,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string current.text_font); *) - !refresh_font_hook ()) + !refresh_editor_hook ()) true in @@ -464,7 +461,7 @@ let configure ?(apply=(fun () -> ())) () = current.background_color <- Tags.string_of_color background_button#color; current.processing_color <- Tags.string_of_color processing_button#color; current.processed_color <- Tags.string_of_color processed_button#color; - !refresh_background_color_hook (); + !refresh_editor_hook (); Tags.set_processing_color processing_button#color; Tags.set_processed_color processed_button#color in @@ -548,7 +545,7 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> current.auto_complete <- s; - !auto_complete_hook s) + !refresh_editor_hook ()) "Auto Complete" current.auto_complete in diff --git a/ide/preferences.mli b/ide/preferences.mli index 7a5e73570..3003715f6 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -87,10 +87,8 @@ val current : pref val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) -val refresh_font_hook : (unit -> unit) ref val refresh_editor_hook : (unit -> unit) ref val refresh_style_hook : (unit -> unit) ref -val refresh_background_color_hook : (unit -> unit) ref val refresh_toolbar_hook : (unit -> unit) ref val resize_window_hook : (unit -> unit) ref val refresh_tabs_hook : (unit -> unit) ref diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 64f7da101..cbc8212e9 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -8,6 +8,8 @@ open Ideutils open GText +open Gtk_parsing + type action = | Insert of string * int * int (* content*pos*length *) | Delete of string * int * int (* content*pos*length *) @@ -18,15 +20,60 @@ let neg act = match act with type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj +let is_substring s1 s2 = + let s1 = Glib.Utf8.to_unistring s1 in + let s2 = Glib.Utf8.to_unistring s2 in + let break = ref true in + let i = ref 0 in + let len1 = Array.length s1 in + let len2 = Array.length s2 in + while !break && !i < len1 & !i < len2 do + break := s1.(!i) = s2.(!i); + incr i; + done; + if !break then len2 - len1 + else -1 + +module StringOrd = +struct + type t = string + let compare = Pervasives.compare +end + +module Proposals = Set.Make(StringOrd) + +let get_completion (buffer : GText.buffer) w = + let rec get_aux accu (iter : GText.iter) = + match iter#forward_search w with + | None -> accu + | Some (start, stop) -> + if starts_word start then + let ne = find_word_end stop in + if ne#compare stop = 0 then get_aux accu stop + else + let proposal = buffer#get_text ~start ~stop:ne () in + get_aux (Proposals.add proposal accu) stop + else get_aux accu stop + in + get_aux Proposals.empty buffer#start_iter + class script_view (tv : source_view) = object (self) inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super val mutable history = [] val mutable redo = [] + val mutable auto_complete = false + val mutable auto_complete_length = 3 + val mutable last_completion = (-1, "", Proposals.empty) val undo_lock = Mutex.create () + method auto_complete = auto_complete + + method set_auto_complete flag = + auto_complete <- flag + method private dump_debug () = let iter = function | Insert (s, p, l) -> @@ -114,9 +161,54 @@ object (self) Mutex.unlock undo_lock end + method private do_auto_complete () = + let iter = self#buffer#get_iter `INSERT in + prerr_endline ("Completion at offset: " ^ string_of_int iter#offset); + let start = find_word_start iter in + if ends_word iter#backward_char then begin + let w = self#buffer#get_text ~start ~stop:iter () in + if String.length w >= auto_complete_length then begin + prerr_endline ("Completion of prefix: '" ^ w ^ "'"); + let (off, prefix, proposals) = last_completion in + let new_proposals = + (* check whether we have the last request in cache *) + 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 () = last_completion <- (start#offset, w, ans) in + ans + in + let prop = + try Some (Proposals.choose new_proposals) + with Not_found -> None + in + match prop with + | None -> () + | Some proposal -> + let suffix = + let len1 = String.length proposal in + let len2 = String.length w in + String.sub proposal len2 (len1 - len2) + in + let offset = iter#offset in + ignore (self#buffer#delete_selection ()); + ignore (self#buffer#insert_interactive suffix); + let ins = self#buffer#get_iter (`OFFSET offset) in + let sel = self#buffer#get_iter `INSERT in + self#buffer#select_range sel ins + end + end + + method private may_auto_complete iter s = + if auto_complete then self#do_auto_complete () + initializer + (* Install undo managing *) ignore (self#buffer#connect#insert_text ~callback:self#handle_insert); ignore (self#buffer#connect#delete_range ~callback:self#handle_delete); + (* Install auto-completion *) + ignore (self#buffer#connect#after#insert_text ~callback:self#may_auto_complete); (* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *) ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit())); ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit())); diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index bc738257c..a2024eeec 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -16,6 +16,8 @@ object method undo : unit -> bool method redo : unit -> bool method clear_undo : unit -> unit + method auto_complete : bool + method set_auto_complete : bool -> unit end val script_view : |