(************************************************************************)
(*  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)