diff options
| -rw-r--r-- | ide/coqide.ml | 54 | ||||
| -rw-r--r-- | ide/highlight.mll | 24 | ||||
| -rw-r--r-- | ide/ideutils.ml | 5 | ||||
| -rw-r--r-- | ide/ideutils.mli | 5 |
4 files changed, 61 insertions, 27 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index e2f4fddc3..22aa9a41b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -166,6 +166,7 @@ object('self) GText.iter -> (GText.iter * GText.iter) option method get_insert : GText.iter method get_start_of_input : GText.iter + method indent_current_line : unit method insert_command : string -> string -> unit method insert_commands : (string * string) list -> unit method insert_message : string -> unit @@ -325,8 +326,6 @@ let remove_current_view_page () = kill_input_view c; ((notebook ())#get_nth_page c)#misc#hide () -let underscore = Glib.Utf8.to_unichar "_" (ref 0) -let bn = Glib.Utf8.to_unichar "\n" (ref 0) let starts_word it = it#starts_word && it#backward_char#char <> underscore let ends_word it = it#ends_line || (it#ends_word && it#char <> underscore) @@ -706,6 +705,37 @@ object(self) ~within_margin:0.25) `INSERT) + + method indent_current_line = + let get_nb_space it = + let it = it#copy in + let nb_sep = ref 0 in + let continue = ref true in + while !continue do + if it#char = space then begin + incr nb_sep; + if not it#nocopy#forward_char then continue := false; + end else continue := false + done; + !nb_sep + in + let previous_line = self#get_insert in + if previous_line#nocopy#backward_line then begin + let previous_line_spaces = get_nb_space previous_line in + let current_line_start = self#get_insert#set_line_offset 0 in + let current_line_spaces = get_nb_space current_line_start in + if input_buffer#delete_interactive + ~start:current_line_start + ~stop:(current_line_start#forward_chars current_line_spaces) + () + then + let current_line_start = self#get_insert#set_line_offset 0 in + input_buffer#insert + ~iter:current_line_start + (String.make previous_line_spaces ' ') + end + + method show_goals = try proof_view#buffer#set_text ""; @@ -1329,7 +1359,12 @@ Please restart and report NOW."; if GdkKeysyms._Break=k then break (); false - | l -> false + | l -> + if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin + prerr_endline "active_kp_handler for Tab"; + self#indent_current_line; + true + end else false end method disconnected_keypress_handler k = match GdkEvent.Key.state k with @@ -1482,8 +1517,8 @@ Please restart and report NOW."; ~start:self#get_start_of_input ~stop "error"; - Highlight.highlight_slice - input_buffer self#get_start_of_input stop + Highlight.highlight_around_current_line + input_buffer ) ); ignore (input_buffer#add_selection_clipboard (cb())); @@ -1850,7 +1885,7 @@ let main files = let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in ignore (rehighlight_m#connect#activate (fun () -> - Highlight.rehighlight_all + Highlight.highlight_all (get_current_view()).view#buffer; (out_some (get_current_view()).analyzed_view)#recenter_insert)); @@ -1914,7 +1949,7 @@ let main files = ~callback:(fun b -> () ) in -(* read_only_i#misc#set_state `INSENSITIVE;*) + read_only_i#misc#set_state `INSENSITIVE; let search_if = edit_f#add_item "Search _forward" ~key:GdkKeysyms._greater @@ -1929,9 +1964,11 @@ let main files = (fun b -> let v = out_some (get_current_view ()).analyzed_view - in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) + in v#complete_at_offset + ((v#view#buffer#get_iter `SEL_BOUND)#offset) )) in + to_do_on_page_switch := (fun i -> @@ -2113,7 +2150,6 @@ let main files = view#buffer#move_mark `INSERT iter; ignore (iter#nocopy#backward_chars len); view#buffer#move_mark `SEL_BOUND iter; - Highlight.highlight_all view#buffer end) in ignore (templates_factory#add_item menu_text ~callback ?key) diff --git a/ide/highlight.mll b/ide/highlight.mll index cdfc51f98..dcb16281b 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -75,7 +75,12 @@ and comment = parse if !highlighting then prerr_endline "Rejected highlight" else begin highlighting := true; - prerr_endline "Highlighting now"; + prerr_endline "Highlighting slice now"; + input_buffer#remove_tag_by_name ~start ~stop "error"; + input_buffer#remove_tag_by_name ~start ~stop "kwd"; + input_buffer#remove_tag_by_name ~start ~stop "decl"; + input_buffer#remove_tag_by_name ~start ~stop "comment"; + (try begin let offset = start#offset in let s = start#get_slice ~stop in @@ -87,9 +92,6 @@ and comment = parse let b,e = convert_pos b,convert_pos e in let start = input_buffer#get_iter_at_char (offset + b) in let stop = input_buffer#get_iter_at_char (offset + e) in - input_buffer#remove_tag_by_name ~start ~stop "kwd"; - input_buffer#remove_tag_by_name ~start ~stop "decl"; - input_buffer#remove_tag_by_name ~start ~stop "comment"; input_buffer#apply_tag_by_name ~start ~stop o done with End_of_file -> () @@ -118,18 +120,4 @@ and comment = parse highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter with _ -> () - let rehighlight_all (input_buffer:GText.buffer) = - input_buffer#remove_tag_by_name - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter "comment"; - input_buffer#remove_tag_by_name - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter "kwd"; - input_buffer#remove_tag_by_name - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter "decl"; - input_buffer#remove_tag_by_name - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter "error"; - highlight_all input_buffer } diff --git a/ide/ideutils.ml b/ide/ideutils.ml index f8af156c4..e1c1a2f64 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -261,3 +261,8 @@ let run_command f c = Buffer.add_string result r done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) + +let underscore = Glib.Utf8.to_unichar "_" (ref 0) +let bn = Glib.Utf8.to_unichar "\n" (ref 0) +let space = Glib.Utf8.to_unichar " " (ref 0) +let tab = Glib.Utf8.to_unichar "\t" (ref 0) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 011fd6d85..3edc8ef85 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -47,3 +47,8 @@ open Format val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit val run_command : (string -> unit) -> string -> Unix.process_status*string + +val underscore : Glib.unichar +val bn : Glib.unichar +val space : Glib.unichar +val tab : Glib.unichar |