diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/gtk_parsing.ml | 71 | ||||
| -rw-r--r-- | ide/session.ml | 6 | ||||
| -rw-r--r-- | ide/session.mli | 2 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
5 files changed, 42 insertions, 41 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 70fa61b208..14cd87e7b5 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -966,6 +966,8 @@ let build_ui () = with _ -> () in let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in + let _ = w#misc#connect#size_allocate + ~callback:(fun rect -> window_size := (rect.Gtk.width, rect.Gtk.height)) in let _ = set_drag w#drag in let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index a84c161a84..8e6d9f75c7 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -12,50 +12,45 @@ let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0) let dot = Glib.Utf8.to_unichar "." ~pos:(ref 0) -(* TODO: avoid num and prime at the head of a word *) -let is_word_char c = - Glib.Unichar.isalnum c || c = underscore || c = prime || c = dot +let find_word_start (it:GText.iter) = + let rec aux it good = + if it#is_start then good + else + let it = it#backward_char in + let c = it#char in + if Glib.Unichar.isalpha c || c = underscore then aux it it + else if Glib.Unichar.isalnum c || c = prime || c = dot then aux it good + else good in + aux it it +let find_word_end (it:GText.iter) = + let rec aux it good = + if it#is_end then good + else + let c = it#char in + let it = it#forward_char in + if Glib.Unichar.isalnum c || c = prime || c = underscore then aux it it + else if c = dot then aux it good + else good in + aux it it let starts_word (it:GText.iter) = - (it#is_start || - (let c = it#backward_char#char in - not (is_word_char c))) + if it#is_start then true + else + let it = it#backward_char in + let c = it#char in + if Glib.Unichar.isalpha c || c = underscore then + it#equal (find_word_start it) + else false let ends_word (it:GText.iter) = - (it#is_end || - let c = it#forward_char#char in - not (is_word_char c) - ) - -let find_word_start (it:GText.iter) = - let rec step_to_start it = - Minilib.log "Find word start"; - if not it#nocopy#backward_char then - (Minilib.log "find_word_start: cannot backward"; it) - else if is_word_char it#char - then step_to_start it - else begin - ignore(it#nocopy#forward_char); - Minilib.log ("Word start at: "^(string_of_int it#offset)); - it - end - in - step_to_start it#copy - -let find_word_end (it:GText.iter) = - let rec step_to_end (it:GText.iter) = - Minilib.log "Find word end"; + if it#is_end then true + else let c = it#char in - if c<>0 && is_word_char c then ( - ignore (it#nocopy#forward_char); - step_to_end it - ) else ( - Minilib.log ("Word end at: "^(string_of_int it#offset)); - it) - in - step_to_end it#copy - + let it = it#forward_char in + if Glib.Unichar.isalnum c || c = prime || c = underscore then + it#equal (find_word_end it) + else false let get_word_around (it:GText.iter) = let start = find_word_start it in diff --git a/ide/session.ml b/ide/session.ml index 38fdd0ef2a..2824530c43 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -432,6 +432,8 @@ let kill (sn:session) = sn.script#destroy (); Coq.close_coqtop sn.coqtop +let window_size = ref (window_width#get, window_height#get) + let build_layout (sn:session) = let session_paned = GPack.paned `VERTICAL () in let session_box = @@ -514,9 +516,9 @@ let build_layout (sn:session) = iteration of the loop *) let () = (* 14 is the estimated size for vertical borders *) - let estimated_vertical_handle_position = (window_width#get - 14) / 2 in + let estimated_vertical_handle_position = (fst !window_size - 14) / 2 in (* 169 is the estimated size for menus, command line, horizontal border *) - let estimated_horizontal_handle_position = (window_height#get - 169) / 2 in + let estimated_horizontal_handle_position = (snd !window_size - 169) / 2 in if estimated_vertical_handle_position > 0 then eval_paned#set_position estimated_vertical_handle_position; if estimated_horizontal_handle_position > 0 then diff --git a/ide/session.mli b/ide/session.mli index f5d8d7c991..63ac1e6dc0 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -51,3 +51,5 @@ val kill : session -> unit val build_layout : session -> GObj.widget option * GObj.widget option * GObj.widget + +val window_size : (int * int) ref diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 98390e810f..ac6712909e 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -175,7 +175,7 @@ object (self) let log = Printf.sprintf "Completion at offset: %i" insert_offset in let () = Minilib.log log in let prefix = - if Gtk_parsing.ends_word iter#backward_char then + 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) |