diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /ide/gtk_parsing.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'ide/gtk_parsing.ml')
-rw-r--r-- | ide/gtk_parsing.ml | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml new file mode 100644 index 00000000..e92a345e --- /dev/null +++ b/ide/gtk_parsing.ml @@ -0,0 +1,176 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: coqide.ml 11952 2009-03-02 15:29:08Z vgross $ *) + +open Ideutils + + +let underscore = Glib.Utf8.to_unichar "_" (ref 0) +let arobase = Glib.Utf8.to_unichar "@" (ref 0) +let prime = 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) + + +(* TODO: avoid num and prime at the head of a word *) +let is_word_char c = + Glib.Unichar.isalnum c || c = underscore || c = prime + + +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))) + + +let ends_word (it:GText.iter) = + (not it#copy#nocopy#forward_char || + let c = it#forward_char#char in + not (is_word_char c) + ) + + +let inside_word (it:GText.iter) = + let c = it#char in + not (starts_word it) && + not (ends_word it) && + is_word_char c + + +let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it + + +let find_word_start (it:GText.iter) = + let rec step_to_start it = + prerr_endline "Find word start"; + if not it#nocopy#backward_char then + (prerr_endline "find_word_start: cannot backward"; it) + else if is_word_char it#char + then step_to_start it + else (it#nocopy#forward_char; + prerr_endline ("Word start at: "^(string_of_int it#offset));it) + 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"; + let c = it#char in + if c<>0 && is_word_char c then ( + ignore (it#nocopy#forward_char); + step_to_end it + ) else ( + prerr_endline ("Word end at: "^(string_of_int it#offset)); + it) + in + step_to_end it#copy + + +let get_word_around (it:GText.iter) = + let start = find_word_start it in + let stop = find_word_end it in + start,stop + + +let rec complete_backward w (it:GText.iter) = + prerr_endline "Complete backward..."; + match it#backward_search w with + | None -> (prerr_endline "backward_search failed";None) + | Some (start,stop) -> + prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); + if starts_word start then + let ne = find_word_end stop in + if ne#compare stop = 0 + then complete_backward w start + else Some (start,stop,ne) + else complete_backward w start + + +let rec complete_forward w (it:GText.iter) = + prerr_endline "Complete forward..."; + match it#forward_search w with + | None -> None + | Some (start,stop) -> + if starts_word start then + let ne = find_word_end stop in + if ne#compare stop = 0 then + complete_forward w stop + else Some (stop,stop,ne) + else complete_forward w stop + + +let find_comment_end (start:GText.iter) = + let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = + match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with + | None,_ -> comment_end + | Some _, None -> raise Not_found + | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> + find_nested_comment next_search_start next_search_end next_comment_end + in + match start#forward_search "*)" with + | None -> raise Not_found + | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end + + +let rec find_string_end (start:GText.iter) = + let dblquote = int_of_char '"' in + let rec escaped_dblquote c = + (c#char = dblquote) && not (escaped_dblquote c#backward_char) + in + match start#forward_search "\"" with + | None -> raise Not_found + | Some (stop,next_start) -> + if escaped_dblquote stop#backward_char + then find_string_end next_start + else next_start + + +let rec find_next_sentence (from:GText.iter) = + match (from#forward_search ".") with + | None -> raise Not_found + | Some (non_vernac_search_end,next_sentence) -> + match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with + | None,None -> + if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 + then next_sentence else find_next_sentence next_sentence + | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) + | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) + | Some (_,comment_search_start),Some (_,string_search_start) -> + find_next_sentence ( + if comment_search_start#compare string_search_start < 0 + then find_comment_end comment_search_start + else find_string_end string_search_start) + + +let find_nearest_forward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#forward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + + +let find_nearest_backward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#backward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + |