1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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
|
