Coqide: some more refactoring to lighten coqide.ml

 Main victim is analyzed_view :
  - some unnecessary methods have been killed (hep_for_keyword for instance)
  - some other migrated elsewhere (recenter_input, find_next_occurrence, ...)
  - analyzed_view is now split in two : fileops (filename, save, revert, ...)
    and coqops (process_next_phrase, ...)

 Four new files created:
 - Sentence (for tag_on_insert and alii)
 - FileOps (ex-first-half of analyzed_view)
 - CoqOps (ex-second-half of analyzed_view)
 - Session (ex-record viewable_script and functions about it)

 Also lots of renaming, trying to be shorter (but still meaningful) and
 more uniform

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 126 insertions, 0 deletions

diff --git a/ide/sentence.ml b/ide/sentence.ml
new file mode 100644
index 000000000..5c61f98de
--- /dev/null
+++ b/ide/sentence.ml
@@ -0,0 +1,126 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** {1 Sentences in coqide buffers } *)
+
+(** Cut a part of the buffer in sentences and tag them.
+    Invariant: either this slice ends the buffer, or it ends with ".".
+    May raise [Coq_lex.Unterminated] when the zone ends with
+    an unterminated sentence. *)
+
+let split_slice_lax (buffer:GText.buffer) start stop =
+  buffer#remove_tag ~start ~stop Tags.Script.comment_sentence;
+  buffer#remove_tag ~start ~stop Tags.Script.sentence;
+  let slice = buffer#get_text ~start ~stop () in
+  let mkiter =
+    (* caveat : partial application with effects *)
+    let convert = Ideutils.byte_offset_to_char_offset slice in
+    fun off -> start#forward_chars (convert off)
+  in
+  let apply_tag off tag =
+    let start = mkiter off in
+    buffer#apply_tag ~start ~stop:start#forward_char tag
+  in
+  Coq_lex.delimit_sentences apply_tag slice
+
+(** Searching forward and backward a position fulfilling some condition *)
+
+let rec forward_search cond (iter:GText.iter) =
+  if iter#is_end || cond iter then iter
+  else forward_search cond iter#forward_char
+
+let rec backward_search cond (iter:GText.iter) =
+  if iter#is_start || cond iter then iter
+  else backward_search cond iter#backward_char
+
+let is_sentence_end s =
+  s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence
+
+let is_char s c = s#char = Char.code c
+
+(** Search backward the first character of a sentence, starting at [iter]
+    and going at most up to [soi] (meant to be the end of the locked zone).
+    Raise [StartError] when no proper sentence start has been found.
+    A character following a ending "." is considered as a sentence start
+    only if this character is a blank. In particular, when a final "."
+    at the end of the locked zone isn't followed by a blank, then this
+    non-blank character will be signaled as erroneous in [tag_on_insert] below.
+*)
+
+exception StartError
+
+let grab_sentence_start (iter:GText.iter) soi =
+  let cond iter =
+    if iter#compare soi < 0 then raise StartError;
+    let prev = iter#backward_char in
+    is_sentence_end prev &&
+      (not (is_char prev '.') ||
+       List.exists (is_char iter) [' ';'\n';'\r';'\t'])
+  in
+  backward_search cond iter
+
+(** Search forward the first character immediately after a sentence end *)
+
+let rec grab_sentence_stop (start:GText.iter) =
+  (forward_search is_sentence_end start)#forward_char
+
+(** Search forward the first character immediately after a "." sentence end
+    (and not just a "{" or "}" or comment end *)
+
+let rec grab_ending_dot (start:GText.iter) =
+  let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
+  (forward_search is_ending_dot start)#forward_char
+
+(** Retag a zone that has been edited *)
+
+let tag_on_insert buffer =
+  (* the start of the non-locked zone *)
+  let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
+  (* the inserted zone is between [prev_insert] and [insert] *)
+  let insert = buffer#get_iter_at_mark `INSERT in
+  let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
+  (* [prev] is normally always before [insert] even when deleting.
+     Let's check this nonetheless *)
+  let prev, insert =
+    if insert#compare prev < 0 then insert, prev else prev, insert
+  in
+  try
+    let start = grab_sentence_start prev soi in
+    (** The status of "{" "}" as sentence delimiters is too fragile.
+        We retag up to the next "." instead. *)
+    let stop = grab_ending_dot insert in
+    try split_slice_lax buffer start stop
+    with Coq_lex.Unterminated ->
+      (* This shouldn't happen frequently. Either:
+         - we are at eof, with indeed an unfinished sentence.
+         - we have just inserted an opening of comment or string.
+         - the inserted text ends with a "." that interacts with the "."
+           found by [grab_ending_dot] to form a non-ending "..".
+         In any case, we retag up to eof, since this isn't that costly. *)
+      if not stop#is_end then
+        try split_slice_lax buffer start buffer#end_iter
+        with Coq_lex.Unterminated -> ()
+  with StartError ->
+    buffer#apply_tag ~start:soi ~stop:soi#forward_char Tags.Script.error
+
+let tag_all buffer =
+  try split_slice_lax buffer buffer#start_iter buffer#end_iter
+  with Coq_lex.Unterminated -> ()
+
+(** Search a sentence around some position *)
+
+let find buffer (start:GText.iter) =
+  let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
+  try
+    let start = grab_sentence_start start soi in
+    let stop = grab_sentence_stop start in
+    (* Is this phrase non-empty and complete ? *)
+    if stop#compare start > 0 && is_sentence_end stop#backward_char
+    then Some (start,stop)
+    else None
+  with StartError -> None