aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/gtk_parsing.ml
blob: f905053ddbaf5db4994a03b6a76468f15efbb6b0 (plain)
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
177
178
179
180
181
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0)
let space = Glib.Utf8.to_unichar " " ~pos:(ref 0)
let tab = Glib.Utf8.to_unichar "\t" ~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


let starts_word (it:GText.iter) =
  (it#is_start ||
    (let c = it#backward_char#char in
      not (is_word_char c)))

let ends_word (it:GText.iter) =
  (it#is_end ||
     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 =
    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 (it#nocopy#forward_char;
	Minilib.log ("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) =
    Minilib.log "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 (
      Minilib.log ("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) =
  Minilib.log "Complete backward...";
  match it#backward_search w with
    | None -> (Minilib.log "backward_search failed";None)
    | Some (start,stop) ->
	Minilib.log ("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) =
  Minilib.log "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

(** On double-click on a view, select the whole word. This is a workaround for
    a deficient word handling in TextView. *)
let fix_double_click self =
  let callback ev = match GdkEvent.get_type ev with
  | `TWO_BUTTON_PRESS ->
    let iter = self#buffer#get_iter `INSERT in
    let start, stop = get_word_around iter in
    let () = self#buffer#move_mark `INSERT ~where:start in
    let () = self#buffer#move_mark `SEL_BOUND ~where:stop in
    true
  | _ -> false
  in
  ignore (self#event#connect#button_press ~callback)