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

16 files changed, 1303 insertions, 1150 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
new file mode 100644
index 000000000..6d99077be
--- /dev/null
+++ b/ide/coqOps.ml
@@ -0,0 +1,432 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Ideutils
+
+type flag = [ `COMMENT | `UNSAFE ]
+
+type ide_info = {
+  start : GText.mark;
+  stop : GText.mark;
+  flags : flag list;
+}
+
+let prefs = Preferences.current
+
+class type ops =
+object
+  method go_to_insert : Coq.task
+  method tactic_wizard : string list -> Coq.task
+  method process_next_phrase : Coq.task
+  method process_until_end_or_error : Coq.task
+  method handle_reset_initial : Coq.reset_kind -> Coq.task
+  method raw_coq_query : string -> Coq.task
+  method show_goals : Coq.task
+  method backtrack_last_phrase : Coq.task
+  method include_file_dir_in_path : Coq.task
+end
+
+class coqops
+  (_script:Wg_ScriptView.script_view)
+  (_pv:Wg_ProofView.proof_view)
+  (_mv:Wg_MessageView.message_view)
+  get_filename =
+object(self)
+  val script = _script
+  val buffer = (_script#source_buffer :> GText.buffer)
+  val proof = _pv
+  val messages = _mv
+
+  val cmd_stack = Stack.create ()
+
+  method private get_start_of_input =
+    buffer#get_iter_at_mark (`NAME "start_of_input")
+
+  method private get_insert =
+    buffer#get_iter_at_mark `INSERT
+
+  method show_goals h k =
+    Coq.PrintOpt.set_printing_width proof#width;
+    Coq.goals h (function
+      |Interface.Fail (l, str) ->
+        (messages#set ("Error in coqtop:\n"^str); k())
+      |Interface.Good goals | Interface.Unsafe goals ->
+        Coq.evars h (function
+          |Interface.Fail (l, str)->
+            (messages#set ("Error in coqtop:\n"^str); k())
+          |Interface.Good evs | Interface.Unsafe evs ->
+            proof#set_goals goals;
+            proof#set_evars evs;
+            proof#refresh ();
+            k()))
+
+  (* This method is intended to perform stateless commands *)
+  method raw_coq_query phrase h k =
+    let () = Minilib.log "raw_coq_query starting now" in
+    let display_error s =
+      if not (Glib.Utf8.validate s) then
+        flash_info "This error is so nasty that I can't even display it."
+      else messages#add s;
+    in
+    Coq.interp ~logger:messages#push ~raw:true ~verbose:false phrase h
+      (function
+        | Interface.Fail (_, err) -> display_error err; k ()
+        | Interface.Good msg | Interface.Unsafe msg ->
+          messages#add msg; k ())
+
+  (** [fill_command_queue until q] fills a command queue until the [until]
+      condition returns true; it is fed with the number of phrases read and the
+      iters enclosing the current sentence. *)
+  method private fill_command_queue until queue =
+    let rec loop len iter =
+      match Sentence.find buffer iter with
+      | None -> raise Exit
+      | Some (start, stop) ->
+        if until len start stop then raise Exit;
+        buffer#apply_tag Tags.Script.to_process ~start ~stop;
+        (* Check if this is a comment *)
+        let is_comment =
+          stop#backward_char#has_tag Tags.Script.comment_sentence
+        in
+        let payload = {
+          start = `MARK (buffer#create_mark start);
+          stop = `MARK (buffer#create_mark stop);
+          flags = if is_comment then [`COMMENT] else [];
+        } in
+        Queue.push payload queue;
+        if not stop#is_end then loop (succ len) stop
+    in
+    try loop 0 self#get_start_of_input with Exit -> ()
+
+  method private discard_command_queue queue =
+    while not (Queue.is_empty queue) do
+      let sentence = Queue.pop queue in
+      let start = buffer#get_iter_at_mark sentence.start in
+      let stop = buffer#get_iter_at_mark sentence.stop in
+      buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      buffer#delete_mark sentence.start;
+      buffer#delete_mark sentence.stop;
+    done
+
+  method private commit_queue_transaction queue sentence newflags =
+    (* A queued command has been successfully done, we push it to [cmd_stack].
+       We reget the iters here because Gtk is unable to warranty that they
+       were not modified meanwhile. Not really necessary but who knows... *)
+    let start = buffer#get_iter_at_mark sentence.start in
+    let stop = buffer#get_iter_at_mark sentence.stop in
+    let sentence = { sentence with flags = newflags @ sentence.flags } in
+    let tag =
+      if List.mem `UNSAFE newflags then Tags.Script.unjustified
+      else Tags.Script.processed
+    in
+    buffer#move_mark ~where:stop (`NAME "start_of_input");
+    buffer#apply_tag tag ~start ~stop;
+    buffer#remove_tag Tags.Script.to_process ~start ~stop;
+    ignore (Queue.pop queue);
+    Stack.push sentence cmd_stack
+
+  method private process_error queue phrase loc msg h k =
+    let position_error = function
+      | None -> ()
+      | Some (start, stop) ->
+        let soi = self#get_start_of_input in
+        let start =
+          soi#forward_chars (byte_offset_to_char_offset phrase start) in
+        let stop =
+          soi#forward_chars (byte_offset_to_char_offset phrase stop) in
+        buffer#apply_tag Tags.Script.error ~start ~stop;
+        buffer#place_cursor ~where:start
+    in
+    self#discard_command_queue queue;
+    pop_info ();
+    position_error loc;
+    messages#clear;
+    messages#push Interface.Error msg;
+    self#show_goals h k
+
+  (** Compute the phrases until [until] returns [true]. *)
+  method private process_until until verbose h k =
+    let queue = Queue.create () in
+    (* Lock everything and fill the waiting queue *)
+    push_info "Coq is computing";
+    messages#clear;
+    script#set_editable false;
+    self#fill_command_queue until queue;
+    (* Now unlock and process asynchronously *)
+    script#set_editable true;
+    let push_info lvl msg = if verbose then messages#push lvl msg
+    in
+    Minilib.log "Begin command processing";
+    let rec loop () =
+      if Queue.is_empty queue then
+        let () = pop_info () in
+        let () = script#recenter_insert in
+        self#show_goals h k
+      else
+        let sentence = Queue.peek queue in
+        if List.mem `COMMENT sentence.flags then
+          (self#commit_queue_transaction queue sentence []; loop ())
+        else
+          (* If the line is not a comment, we interpret it. *)
+          let start = buffer#get_iter_at_mark sentence.start in
+          let stop = buffer#get_iter_at_mark sentence.stop in
+          let phrase = start#get_slice ~stop in
+          let commit_and_continue msg flags =
+            push_info Interface.Notice msg;
+            self#commit_queue_transaction queue sentence flags;
+            loop ()
+          in
+          Coq.interp ~logger:push_info ~verbose phrase h
+            (function
+              |Interface.Good msg -> commit_and_continue msg []
+              |Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
+              |Interface.Fail (loc, msg) ->
+                self#process_error queue phrase loc msg h k)
+    in
+    loop ()
+
+  method process_next_phrase h k =
+    let until len start stop = 1 <= len in
+    self#process_until until true h
+      (fun () -> buffer#place_cursor ~where:self#get_start_of_input; k())
+
+  method private process_until_iter iter h k =
+    let until len start stop =
+      if prefs.Preferences.stop_before then stop#compare iter > 0
+      else start#compare iter >= 0
+    in
+    self#process_until until false h k
+
+  method process_until_end_or_error h k =
+    self#process_until_iter buffer#end_iter h k
+
+  (** Clear the command stack until [until] returns [true].
+      Returns the number of commands sent to Coqtop to backtrack. *)
+  method private clear_command_stack until =
+    let rec loop len real_len =
+      if Stack.is_empty cmd_stack then real_len
+      else
+        let phrase = Stack.top cmd_stack in
+        let is_comment = List.mem `COMMENT phrase.flags in
+        let start = buffer#get_iter_at_mark phrase.start in
+        let stop = buffer#get_iter_at_mark phrase.stop in
+        if not (until len real_len start stop) then begin
+          (* [until] has not been reached, so we clear this command *)
+          ignore (Stack.pop cmd_stack);
+          buffer#remove_tag Tags.Script.processed ~start ~stop;
+          buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+          buffer#move_mark ~where:start (`NAME "start_of_input");
+          buffer#delete_mark phrase.start;
+          buffer#delete_mark phrase.stop;
+          loop (succ len) (if is_comment then real_len else succ real_len)
+        end else
+          real_len
+    in
+    loop 0 0
+
+  (** Actually performs the undoing *)
+  method private undo_command_stack n h k =
+    Coq.rewind n h (function
+      |Interface.Good n | Interface.Unsafe n ->
+        let until _ len _ _ = n <= len in
+        (* Coqtop requested [n] more ACTUAL backtrack *)
+        ignore (self#clear_command_stack until);
+        k ()
+      |Interface.Fail (l, str) ->
+        messages#set
+          ("Error while backtracking: " ^ str ^
+           "\nCoqIDE and coqtop may be out of sync," ^
+           "you may want to use Restart.");
+        k ())
+
+  (** Wrapper around the raw undo command *)
+  method private backtrack_until until h k =
+    push_info "Coq is undoing";
+    messages#clear;
+    (* Lock everything *)
+    script#set_editable false;
+    let to_undo = self#clear_command_stack until in
+    self#undo_command_stack to_undo h
+      (fun () -> script#set_editable true; pop_info (); k ())
+
+  method private backtrack_to_iter iter h k =
+    let until _ _ _ stop = iter#compare stop >= 0 in
+    self#backtrack_until until h
+      (* We may have backtracked too much: let's replay *)
+      (fun () -> self#process_until_iter iter h k)
+
+  method backtrack_last_phrase h k =
+    let until len _ _ _ = 1 <= len in
+    self#backtrack_until until h
+      (fun () ->
+        buffer#place_cursor ~where:self#get_start_of_input;
+        self#show_goals h k)
+
+  method go_to_insert h k =
+    let point = self#get_insert in
+    if point#compare self#get_start_of_input >= 0
+    then self#process_until_iter point h k
+    else self#backtrack_to_iter point h k
+
+  method tactic_wizard l h k =
+    let insert_phrase phrase tag =
+      let stop = self#get_start_of_input in
+      let phrase' = if stop#starts_line then phrase else "\n"^phrase in
+      buffer#insert ~iter:stop phrase';
+      Sentence.tag_on_insert buffer;
+      let start = self#get_start_of_input in
+      buffer#move_mark ~where:stop (`NAME "start_of_input");
+      buffer#apply_tag tag ~start ~stop;
+      if self#get_insert#compare stop <= 0 then
+        buffer#place_cursor ~where:stop;
+      let ide_payload = {
+        start = `MARK (buffer#create_mark start);
+        stop = `MARK (buffer#create_mark stop);
+        flags = [];
+      } in
+      Stack.push ide_payload cmd_stack;
+      messages#clear;
+      self#show_goals h k;
+    in
+    let display_error (loc, s) =
+      if not (Glib.Utf8.validate s) then
+        flash_info "This error is so nasty that I can't even display it."
+      else messages#add s
+    in
+    let try_phrase phrase stop more =
+      Minilib.log "Sending to coq now";
+      Coq.interp ~verbose:false phrase h
+        (function
+          |Interface.Fail (l, str) ->
+            display_error (l, str);
+            messages#add ("Unsuccessfully tried: "^phrase);
+            more ()
+          |Interface.Good msg ->
+            messages#add msg;
+            stop Tags.Script.processed
+          |Interface.Unsafe msg ->
+            messages#add msg;
+            stop Tags.Script.unjustified)
+    in
+    let rec loop l () = match l with
+      | [] -> k ()
+      | p :: l' ->
+        try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
+    in
+    loop l ()
+
+  method handle_reset_initial why h k =
+    if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
+    (* clear the stack *)
+    while not (Stack.is_empty cmd_stack) do
+      let phrase = Stack.pop cmd_stack in
+      buffer#delete_mark phrase.start;
+      buffer#delete_mark phrase.stop
+    done;
+    (* reset the buffer *)
+    let start = buffer#start_iter in
+    let stop = buffer#end_iter in
+    buffer#move_mark ~where:start (`NAME "start_of_input");
+    buffer#remove_tag Tags.Script.processed ~start ~stop;
+    buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+    buffer#remove_tag Tags.Script.to_process ~start ~stop;
+    Sentence.tag_on_insert buffer;
+    (* clear the views *)
+    messages#clear;
+    proof#clear ();
+    clear_info ();
+    push_info "Restarted";
+    (* apply the initial commands to coq *)
+    self#include_file_dir_in_path h k;
+
+  method include_file_dir_in_path h k =
+    match get_filename () with
+      |None -> k ()
+      |Some f ->
+        let dir = Filename.dirname f in
+        Coq.inloadpath dir h (function
+          |Interface.Fail (_,s) ->
+            messages#set
+              ("Could not determine lodpath, this might lead to problems:\n"^s);
+            k ()
+          |Interface.Good true |Interface.Unsafe true -> k ()
+          |Interface.Good false |Interface.Unsafe false ->
+            let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
+            Coq.interp cmd h (function
+              |Interface.Fail (l,str) ->
+                messages#set ("Couln't add loadpath:\n"^str);
+                k ()
+              |Interface.Good _ | Interface.Unsafe _ -> k ()))
+
+(** NB: Events during text edition:
+
+    - [begin_user_action]
+    - [insert_text] (or [delete_range] when deleting)
+    - [changed]
+    - [end_user_action]
+
+   When pasting a text containing tags (e.g. the sentence terminators),
+   there is actually many [insert_text] and [changed]. For instance,
+   for "a. b.":
+
+    - [begin_user_action]
+    - [insert_text] (for "a")
+    - [changed]
+    - [insert_text] (for ".")
+    - [changed]
+    - [apply_tag] (for the tag of ".")
+    - [insert_text] (for " b")
+    - [changed]
+    - [insert_text] (for ".")
+    - [changed]
+    - [apply_tag] (for the tag of ".")
+    - [end_user_action]
+
+  Since these copy-pasted tags may interact badly with the retag mechanism,
+  we now don't monitor the "changed" event, but rather the "begin_user_action"
+  and "end_user_action". We begin by setting a mark at the initial cursor
+  point. At the end, the zone between the mark and the cursor is to be
+  untagged and then retagged. *)
+
+  initializer
+  let _ = buffer#connect#insert_text
+    ~callback:(fun it s ->
+      (* If a #insert happens in the locked zone, we discard it.
+         Other solution: always use #insert_interactive and similar *)
+      if (it#compare self#get_start_of_input)<0 then
+        GtkSignal.stop_emit ();
+      if String.length s > 1 then
+        let () = Minilib.log "insert_text: Placing cursor" in
+        buffer#place_cursor ~where:it;
+        if String.contains s '\n' then
+          let () = Minilib.log "insert_text: Recentering" in
+          script#recenter_insert)
+  in
+  let _ = buffer#connect#begin_user_action
+    ~callback:(fun () ->
+      let where = self#get_insert in
+      buffer#move_mark (`NAME "prev_insert") ~where;
+      let start = self#get_start_of_input in
+      let stop = buffer#end_iter in
+      buffer#remove_tag Tags.Script.error ~start ~stop)
+  in
+  let _ = buffer#connect#end_user_action
+    ~callback:(fun () -> Sentence.tag_on_insert buffer)
+  in
+  let _ = buffer#connect#after#mark_set
+    ~callback:(fun it m ->
+      !set_location
+        (Printf.sprintf "Line: %5d Char: %3d"
+           (self#get_insert#line + 1)
+           (self#get_insert#line_offset + 1));
+      match GtkText.Mark.get_name m  with
+        | Some "insert" -> ()
+        | Some s -> Minilib.log (s^" moved")
+        | None -> ())
+  in ()
+end
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
new file mode 100644
index 000000000..2a6963fee
--- /dev/null
+++ b/ide/coqOps.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+
+class type ops =
+object
+  method go_to_insert : Coq.task
+  method tactic_wizard : string list -> Coq.task
+  method process_next_phrase : Coq.task
+  method process_until_end_or_error : Coq.task
+  method handle_reset_initial : Coq.reset_kind -> Coq.task
+  method raw_coq_query : string -> Coq.task
+  method show_goals : Coq.task
+  method backtrack_last_phrase : Coq.task
+  method include_file_dir_in_path : Coq.task
+end
+
+class coqops :
+  Wg_ScriptView.script_view ->
+  Wg_ProofView.proof_view ->
+  Wg_MessageView.message_view ->
+  (unit -> string option) ->
+  ops
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f244e630f..bcd638689 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -9,6 +9,7 @@
 open Preferences
 open Gtk_parsing
 open Ideutils
+open Session
 
 (** Note concerning GtkTextBuffer
 
@@ -41,160 +42,51 @@ open Ideutils
    revalidated by the default signal handler.
 *)
 
-type direction = Up | Down
-
-type flag = [ `COMMENT | `UNSAFE ]
-
-type ide_info = {
-  start : GText.mark;
-  stop : GText.mark;
-  flags : flag list;
-}
-
-let revert_timer = Ideutils.mktimer ()
-let autosave_timer = Ideutils.mktimer ()
+(** {2 Some static elements } *)
 
 let prefs = Preferences.current
 
+(** The arguments that will be passed to coqtop. No quoting here, since
+    no /bin/sh when using create_process instead of open_process. *)
+let custom_project_files = ref []
+let sup_args = ref []
+
 let logfile = ref None
 
-class type _analyzed_view =
-object
-  method filename : string option
-  method update_stats : unit
-  method changed_on_disk : bool
-  method revert : unit
-  method auto_save : unit
-  method save : string -> bool
-  method save_as : string -> bool
-  method recenter_insert : unit
-  method insert_message : string -> unit
-  method set_message : string -> unit
-  method find_next_occurrence : direction -> unit
-  method help_for_keyword : unit -> unit
-
-  method go_to_insert : Coq.task
-  method tactic_wizard : string list -> Coq.task
-  method process_next_phrase : Coq.task
-  method process_until_end_or_error : Coq.task
-  method handle_reset_initial : Coq.reset_kind -> Coq.task
-  method raw_coq_query : string -> Coq.task
-  method show_goals : Coq.task
-  method backtrack_last_phrase : Coq.task
-  method include_file_dir_in_path : Coq.task
-end
+(** {2 Notebook of sessions } *)
 
-type viewable_script = {
-  script : Wg_ScriptView.script_view;
-  tab_label : GMisc.label;
-  proof_view : Wg_ProofView.proof_view;
-  message_view : Wg_MessageView.message_view;
-  analyzed_view : _analyzed_view;
-  toplvl : Coq.coqtop;
-  command : Wg_Command.command_window;
-  finder : Wg_Find.finder;
-}
-
-let kill_session s =
-  (* To close the detached views of this script, we call manually
-     [destroy] on it, triggering some callbacks in [detach_view].
-     In a more modern lablgtk, rather use the page-removed signal ? *)
-  s.script#destroy ();
-  Coq.close_coqtop s.toplvl
-
-let build_session s =
-  let session_paned = GPack.paned `VERTICAL () in
-  let session_box =
-    GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) ()
-  in
-  let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
-    ~packing:(session_box#pack ~expand:true) () in
-  let script_frame = GBin.frame ~shadow_type:`IN
-    ~packing:eval_paned#add1 () in
-  let script_scroll = GBin.scrolled_window
-    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
-  let state_paned = GPack.paned `VERTICAL
-    ~packing:eval_paned#add2 () in
-  let proof_frame = GBin.frame ~shadow_type:`IN
-    ~packing:state_paned#add1 () in
-  let proof_scroll = GBin.scrolled_window
-    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in
-  let message_frame = GBin.frame ~shadow_type:`IN
-    ~packing:state_paned#add2 () in
-  let message_scroll = GBin.scrolled_window
-    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in
-  let session_tab = GPack.hbox ~homogeneous:false () in
-  let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
-    ~packing:session_tab#pack () in
-  let _ =
-    s.script#buffer#connect#modified_changed
-      ~callback:(fun () -> if s.script#buffer#modified
-        then img#set_stock `SAVE
-        else img#set_stock `YES) in
-  let _ =
-    eval_paned#misc#connect#size_allocate
-      ~callback:
-      (let old_paned_width = ref 2 in
-       let old_paned_height = ref 2 in
-       fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
-         if !old_paned_width <> paned_width ||
-            !old_paned_height <> paned_height
-         then begin
-           eval_paned#set_position
-             (eval_paned#position * paned_width / !old_paned_width);
-           state_paned#set_position
-             (state_paned#position * paned_height / !old_paned_height);
-           old_paned_width := paned_width;
-           old_paned_height := paned_height;
-	 end)
-  in
-  session_box#pack s.finder#coerce;
-  session_paned#pack2 ~shrink:false ~resize:false (s.command#frame#coerce);
-  script_scroll#add s.script#coerce;
-  proof_scroll#add s.proof_view#coerce;
-  message_scroll#add s.message_view#coerce;
-  session_tab#pack s.tab_label#coerce;
-  img#set_stock `YES;
-  eval_paned#set_position 1;
-  state_paned#set_position 1;
-  (Some session_tab#coerce,None,session_paned#coerce)
-
-let session_notebook =
-  Wg_Notebook.create build_session kill_session
-    ~border_width:2 ~show_border:false ~scrollable:true ()
+(** The main element of coqide is a notebook of session views *)
 
-let current_view () = session_notebook#current_term.analyzed_view
-let current_buffer () = session_notebook#current_term.script#buffer
+let notebook =
+  Wg_Notebook.create Session.build_layout Session.kill
+    ~border_width:2 ~show_border:false ~scrollable:true ()
 
-let cb = GData.clipboard Gdk.Atom.primary
 
-let update_notebook_pos () =
-  let pos = match prefs.vertical_tabs, prefs.opposite_tabs with
-    | false, false -> `TOP
-    | false, true  -> `BOTTOM
-    | true , false -> `LEFT
-    | true , true  -> `RIGHT
-  in
-  session_notebook#set_tab_pos pos
+(** {2 Callback functions for the user interface } *)
 
-exception Unsuccessful
+let current_buffer () = notebook#current_term.buffer
 
-let force_reset_initial () =
-  Minilib.log "Reset Initial";
-  Coq.reset_coqtop session_notebook#current_term.toplvl
+(** Nota: using && here has the advantage of working both under win32 and unix.
+    If someday we want the main command to be tried even if the "cd" has failed,
+    then we should use " ; " under unix but " & " under win32 (cf. #2363). *)
 
-let break () =
-  Minilib.log "User break received";
-  Coq.break_coqtop session_notebook#current_term.toplvl
+let local_cd file =
+  "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
 
-let warn_image =
-  let img = GMisc.image () in
-  img#set_stock `DIALOG_WARNING;
-  img#set_icon_size `DIALOG;
-  img#coerce
+let pr_exit_status = function
+  | Unix.WEXITED 0 -> " succeeded"
+  | _ -> " failed"
 
-let warning msg =
-  GToolbox.message_box ~title:"Warning" ~icon:warn_image msg
+let make_coqtop_args = function
+  |None -> !sup_args
+  |Some the_file ->
+    let get_args f = Project_file.args_from_project f
+      !custom_project_files prefs.project_file_name
+    in
+    match prefs.read_project with
+      |Ignore_args -> !sup_args
+      |Append_args -> get_args the_file @ !sup_args
+      |Subst_args -> get_args the_file
 
 module Opt = Coq.PrintOpt
 
@@ -216,827 +108,7 @@ let print_items = [
    "l",false)
 ]
 
-let get_current_word () = match cb#text with
-  |Some t -> Minilib.log ("get_current_word : selection = " ^ t); t
-  |None ->
-    Minilib.log "get_current_word : none selected";
-    let b = current_buffer () in
-    let it = b#get_iter_at_mark `INSERT in
-    let start = find_word_start it in
-    let stop = find_word_end start in
-    b#move_mark `SEL_BOUND ~where:start;
-    b#move_mark `INSERT ~where:stop;
-    b#get_text ~slice:true ~start ~stop ()
-
-(** 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 = 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 Tags.Script.error ~start:soi ~stop:soi#forward_char
-
-let force_retag buffer =
-  try split_slice_lax buffer buffer#start_iter buffer#end_iter
-  with Coq_lex.Unterminated -> ()
-
-(* GtkSource view should handle that one day !!!
-let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
-  (* move back twice if not into proof_decl,
-   * once if into proof_decl and back_char into_proof_decl,
-   * don't move if into proof_decl and back_char not into proof_decl *)
-  if not (cursor#has_tag Tags.Script.proof_decl) then
-    ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
-  if cursor#backward_char#has_tag Tags.Script.proof_decl then
-    ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
-  let decl_start = cursor in
-  let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in
-  let decl_end = grab_ending_dot decl_start in
-  let prf_end = grab_ending_dot prf_end in
-  let prf_end = prf_end#forward_char in
-  if decl_start#has_tag Tags.Script.folded then (
-    buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
-    buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
-  else (
-    buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
-    buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
-*)
-
-(** The arguments that will be passed to coqtop. No quoting here, since
-    no /bin/sh when using create_process instead of open_process. *)
-let custom_project_files = ref []
-let sup_args = ref []
-
-class analyzed_view (_script:Wg_ScriptView.script_view)
-  (_pv:Wg_ProofView.proof_view) (_mv:Wg_MessageView.message_view) _ct _fn =
-object(self)
-  val input_view = _script
-  val input_buffer = _script#source_buffer
-  val proof_view = _pv
-  val message_view = _mv
-  val cmd_stack = Stack.create ()
-  val mycoqtop = _ct
-
-  val mutable filename = _fn
-  val mutable last_stats = NoSuchFile
-  val mutable last_modification_time = 0.
-  val mutable last_auto_save_time = 0.
-
-  val hidden_proofs = Hashtbl.create 32
-
-  method filename = filename
-
-  method update_stats = match filename with
-    |Some f -> last_stats <- Ideutils.stat f
-    |_ -> ()
-
-  method changed_on_disk = match filename with
-    |None -> false
-    |Some f -> match Ideutils.stat f, last_stats with
-        |MTime cur_mt, MTime last_mt -> cur_mt > last_mt
-        |MTime _, (NoSuchFile|OtherError) -> true
-        |NoSuchFile, MTime _ ->
-          flash_info ("Warning, file not on disk anymore : "^f);
-          false
-        |_ -> false
-
-  method revert =
-    let do_revert f =
-      push_info "Reverting buffer";
-      try
-        Coq.reset_coqtop mycoqtop;
-        let b = Buffer.create 1024 in
-        Ideutils.read_file f b;
-        let s = try_convert (Buffer.contents b) in
-        input_buffer#set_text s;
-        self#update_stats;
-        input_buffer#place_cursor ~where:input_buffer#start_iter;
-        input_buffer#set_modified false;
-        pop_info ();
-        flash_info "Buffer reverted";
-        force_retag (input_buffer :> GText.buffer);
-      with _  ->
-        pop_info ();
-        flash_info "Warning: could not revert buffer";
-    in
-    match filename with
-      | None -> ()
-      | Some f ->
-        if not input_buffer#modified then do_revert f
-        else
-          let answ = GToolbox.question_box
-            ~title:"Modified buffer changed on disk"
-            ~buttons:["Revert from File";
-                      "Overwrite File";
-                      "Disable Auto Revert"]
-            ~default:0
-            ~icon:(stock_to_widget `DIALOG_WARNING)
-            "Some unsaved buffers changed on disk"
-          in
-          match answ with
-            | 1 -> do_revert f
-            | 2 -> if self#save f then flash_info "Overwritten" else
-                flash_info "Could not overwrite file"
-            | _ ->
-              Minilib.log "Auto revert set to false";
-              prefs.global_auto_revert <- false;
-              revert_timer.kill ()
-
-  method save f =
-    if try_export f (input_buffer#get_text ()) then begin
-      filename <- Some f;
-      self#update_stats;
-      input_buffer#set_modified false;
-      (match self#auto_save_name with
-        | None -> ()
-        | Some fn -> try Sys.remove fn with _ -> ());
-      true
-    end
-    else false
-
-  method private auto_save_name =
-    match filename with
-      | None -> None
-      | Some f ->
-        let dir = Filename.dirname f in
-        let base = (fst prefs.auto_save_name) ^
-          (Filename.basename f) ^
-          (snd prefs.auto_save_name)
-        in Some (Filename.concat dir base)
-
-  method private need_auto_save =
-    input_buffer#modified &&
-      last_modification_time > last_auto_save_time
-
-  method auto_save =
-    if self#need_auto_save then begin
-      match self#auto_save_name with
-        | None -> ()
-        | Some fn ->
-          try
-            last_auto_save_time <- Unix.time();
-            Minilib.log ("Autosave time: "^(string_of_float (Unix.time())));
-            if try_export fn (input_buffer#get_text ()) then begin
-              flash_info ~delay:1000 "Autosaved"
-            end
-            else warning
-              ("Autosave failed (check if " ^ fn ^ " is writable)")
-          with _ ->
-            warning ("Autosave: unexpected error while writing "^fn)
-    end
-
-  method save_as f =
-    if not (Sys.file_exists f) then self#save f
-    else
-      let answ = GToolbox.question_box ~title:"File exists on disk"
-        ~buttons:["Overwrite"; "Cancel";]
-        ~default:1
-        ~icon:warn_image
-        ("File "^f^" already exists")
-      in
-      match answ with
-        | 1 -> self#save f
-        | _ -> false
-
-  method insert_message s =
-    message_view#push Interface.Notice s
-
-  method set_message s =
-    message_view#clear ();
-    message_view#push Interface.Notice s
-
-  method private push_message level content =
-    message_view#push level content
-
-  method private get_start_of_input =
-    input_buffer#get_iter_at_mark (`NAME "start_of_input")
-
-  method private get_insert =
-    input_buffer#get_iter_at_mark `INSERT
-
-  method recenter_insert =
-    input_view#scroll_to_mark
-      ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
-
-  method help_for_keyword () =
-    browse_keyword (self#insert_message) (get_current_word ())
-
-  (* go to the next occurrence of the current word, forward or backward *)
-  method find_next_occurrence dir =
-    let b = input_buffer in
-    let start = find_word_start self#get_insert in
-    let stop = find_word_end start in
-    let text = b#get_text ~start ~stop () in
-    let search =
-      if dir=Down then stop#forward_search else start#backward_search
-    in
-    match search text with
-      |None -> ()
-      |Some(where, _) -> b#place_cursor ~where; self#recenter_insert
-
-  method show_goals h k =
-    Coq.PrintOpt.set_printing_width proof_view#width;
-    Coq.goals h (function
-      |Interface.Fail (l, str) ->
-        (self#set_message ("Error in coqtop:\n"^str); k())
-      |Interface.Good goals | Interface.Unsafe goals ->
-        Coq.evars h (function
-          |Interface.Fail (l, str)->
-            (self#set_message ("Error in coqtop:\n"^str); k())
-          |Interface.Good evs | Interface.Unsafe evs ->
-            proof_view#set_goals goals;
-            proof_view#set_evars evs;
-            proof_view#refresh ();
-            k()))
-
-  (* This method is intended to perform stateless commands *)
-  method raw_coq_query phrase h k =
-    let () = Minilib.log "raw_coq_query starting now" in
-    let display_error s =
-      if not (Glib.Utf8.validate s) then
-        flash_info "This error is so nasty that I can't even display it."
-      else self#insert_message s;
-    in
-    Coq.interp ~logger:self#push_message ~raw:true ~verbose:false phrase h
-      (function
-        | Interface.Fail (_, err) -> display_error err; k ()
-        | Interface.Good msg | Interface.Unsafe msg ->
-          self#insert_message msg; k ())
-
-  method private find_phrase_starting_at (start:GText.iter) =
-    try
-      let start = grab_sentence_start start self#get_start_of_input 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 Not_found -> None
-
-  (** [fill_command_queue until q] fills a command queue until the [until]
-      condition returns true; it is fed with the number of phrases read and the
-      iters enclosing the current sentence. *)
-  method private fill_command_queue until queue =
-    let rec loop len iter =
-      let opt_sentence = self#find_phrase_starting_at iter in
-      match opt_sentence with
-      | None -> raise Exit
-      | Some (start, stop) ->
-        if until len start stop then raise Exit;
-        input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
-        (* Check if this is a comment *)
-        let is_comment =
-          stop#backward_char#has_tag Tags.Script.comment_sentence
-        in
-        let payload = {
-          start = `MARK (input_buffer#create_mark start);
-          stop = `MARK (input_buffer#create_mark stop);
-          flags = if is_comment then [`COMMENT] else [];
-        } in
-        Queue.push payload queue;
-        if not stop#is_end then loop (succ len) stop
-    in
-    try loop 0 self#get_start_of_input with Exit -> ()
-
-  method private discard_command_queue queue =
-    while not (Queue.is_empty queue) do
-      let sentence = Queue.pop queue in
-      let start = input_buffer#get_iter_at_mark sentence.start in
-      let stop = input_buffer#get_iter_at_mark sentence.stop in
-      input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      input_buffer#delete_mark sentence.start;
-      input_buffer#delete_mark sentence.stop;
-    done
-
-  method private commit_queue_transaction queue sentence newflags =
-    (* A queued command has been successfully done, we push it to [cmd_stack].
-       We reget the iters here because Gtk is unable to warranty that they
-       were not modified meanwhile. Not really necessary but who knows... *)
-    let start = input_buffer#get_iter_at_mark sentence.start in
-    let stop = input_buffer#get_iter_at_mark sentence.stop in
-    let sentence = { sentence with flags = newflags @ sentence.flags } in
-    let tag =
-      if List.mem `UNSAFE newflags then Tags.Script.unjustified
-      else Tags.Script.processed
-    in
-    input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-    input_buffer#apply_tag tag ~start ~stop;
-    input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
-    ignore (Queue.pop queue);
-    Stack.push sentence cmd_stack
-
-  method private process_error queue phrase loc msg h k =
-    let position_error = function
-      | None -> ()
-      | Some (start, stop) ->
-        let soi = self#get_start_of_input in
-        let start =
-          soi#forward_chars (byte_offset_to_char_offset phrase start) in
-        let stop =
-          soi#forward_chars (byte_offset_to_char_offset phrase stop) in
-        input_buffer#apply_tag Tags.Script.error ~start ~stop;
-        input_buffer#place_cursor ~where:start
-    in
-    self#discard_command_queue queue;
-    pop_info ();
-    position_error loc;
-    message_view#clear ();
-    message_view#push Interface.Error msg;
-    self#show_goals h k
-
-  (** Compute the phrases until [until] returns [true]. *)
-  method private process_until until verbose h k =
-    let queue = Queue.create () in
-    (* Lock everything and fill the waiting queue *)
-    push_info "Coq is computing";
-    message_view#clear ();
-    input_view#set_editable false;
-    self#fill_command_queue until queue;
-    (* Now unlock and process asynchronously *)
-    input_view#set_editable true;
-    let push_info lvl msg = if verbose then self#push_message lvl msg
-    in
-    Minilib.log "Begin command processing";
-    let rec loop () =
-      if Queue.is_empty queue then
-        let () = pop_info () in
-        let () = self#recenter_insert in
-        self#show_goals h k
-      else
-        let sentence = Queue.peek queue in
-        if List.mem `COMMENT sentence.flags then
-          (self#commit_queue_transaction queue sentence []; loop ())
-        else
-          (* If the line is not a comment, we interpret it. *)
-          let start = input_buffer#get_iter_at_mark sentence.start in
-          let stop = input_buffer#get_iter_at_mark sentence.stop in
-          let phrase = start#get_slice ~stop in
-          let commit_and_continue msg flags =
-            push_info Interface.Notice msg;
-            self#commit_queue_transaction queue sentence flags;
-            loop ()
-          in
-          Coq.interp ~logger:push_info ~verbose phrase h
-            (function
-              |Interface.Good msg -> commit_and_continue msg []
-              |Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
-              |Interface.Fail (loc, msg) ->
-                self#process_error queue phrase loc msg h k)
-    in
-    loop ()
-
-  method process_next_phrase h k =
-    let until len start stop = 1 <= len in
-    self#process_until until true h
-      (fun () -> input_buffer#place_cursor ~where:self#get_start_of_input; k())
-
-  method private process_until_iter iter h k =
-    let until len start stop =
-      if prefs.stop_before then stop#compare iter > 0
-      else start#compare iter >= 0
-    in
-    self#process_until until false h k
-
-  method process_until_end_or_error h k =
-    self#process_until_iter input_buffer#end_iter h k
-
-  (** Clear the command stack until [until] returns [true].
-      Returns the number of commands sent to Coqtop to backtrack. *)
-  method private clear_command_stack until =
-    let rec loop len real_len =
-      if Stack.is_empty cmd_stack then real_len
-      else
-        let phrase = Stack.top cmd_stack in
-        let is_comment = List.mem `COMMENT phrase.flags in
-        let start = input_buffer#get_iter_at_mark phrase.start in
-        let stop = input_buffer#get_iter_at_mark phrase.stop in
-        if not (until len real_len start stop) then begin
-          (* [until] has not been reached, so we clear this command *)
-          ignore (Stack.pop cmd_stack);
-          input_buffer#remove_tag Tags.Script.processed ~start ~stop;
-          input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-          input_buffer#move_mark ~where:start (`NAME "start_of_input");
-          input_buffer#delete_mark phrase.start;
-          input_buffer#delete_mark phrase.stop;
-          loop (succ len) (if is_comment then real_len else succ real_len)
-        end else
-          real_len
-    in
-    loop 0 0
-
-  (** Actually performs the undoing *)
-  method private undo_command_stack n h k =
-    Coq.rewind n h (function
-      |Interface.Good n | Interface.Unsafe n ->
-        let until _ len _ _ = n <= len in
-        (* Coqtop requested [n] more ACTUAL backtrack *)
-        ignore (self#clear_command_stack until);
-        k ()
-      |Interface.Fail (l, str) ->
-        self#set_message
-          ("Error while backtracking: " ^ str ^
-           "\nCoqIDE and coqtop may be out of sync," ^
-           "you may want to use Restart.");
-        k ())
-
-  (** Wrapper around the raw undo command *)
-  method private backtrack_until until h k =
-    push_info "Coq is undoing";
-    message_view#clear ();
-    (* Lock everything *)
-    input_view#set_editable false;
-    let to_undo = self#clear_command_stack until in
-    self#undo_command_stack to_undo h
-      (fun () -> input_view#set_editable true; pop_info (); k ())
-
-  method private backtrack_to_iter iter h k =
-    let until _ _ _ stop = iter#compare stop >= 0 in
-    self#backtrack_until until h
-      (* We may have backtracked too much: let's replay *)
-      (fun () -> self#process_until_iter iter h k)
-
-  method backtrack_last_phrase h k =
-    let until len _ _ _ = 1 <= len in
-    self#backtrack_until until h
-      (fun () ->
-        input_buffer#place_cursor ~where:self#get_start_of_input;
-        self#show_goals h k)
-
-  method go_to_insert h k =
-    let point = self#get_insert in
-    if point#compare self#get_start_of_input >= 0
-    then self#process_until_iter point h k
-    else self#backtrack_to_iter point h k
-
-  method tactic_wizard l h k =
-    let insert_phrase phrase tag =
-      let stop = self#get_start_of_input in
-      let phrase' = if stop#starts_line then phrase else "\n"^phrase in
-      input_buffer#insert ~iter:stop phrase';
-      tag_on_insert (input_buffer :> GText.buffer);
-      let start = self#get_start_of_input in
-      input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-      input_buffer#apply_tag tag ~start ~stop;
-      if self#get_insert#compare stop <= 0 then
-        input_buffer#place_cursor ~where:stop;
-      let ide_payload = {
-        start = `MARK (input_buffer#create_mark start);
-        stop = `MARK (input_buffer#create_mark stop);
-        flags = [];
-      } in
-      Stack.push ide_payload cmd_stack;
-      message_view#clear ();
-      self#show_goals h k;
-    in
-    let display_error (loc, s) =
-      if not (Glib.Utf8.validate s) then
-        flash_info "This error is so nasty that I can't even display it."
-      else self#insert_message s
-    in
-    let try_phrase phrase stop more =
-      Minilib.log "Sending to coq now";
-      Coq.interp ~verbose:false phrase h
-        (function
-          |Interface.Fail (l, str) ->
-            display_error (l, str);
-            self#insert_message ("Unsuccessfully tried: "^phrase);
-            more ()
-          |Interface.Good msg ->
-            self#insert_message msg;
-            stop Tags.Script.processed
-          |Interface.Unsafe msg ->
-            self#insert_message msg;
-            stop Tags.Script.unjustified)
-    in
-    let rec loop l () = match l with
-      | [] -> k ()
-      | p :: l' ->
-        try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
-    in
-    loop l ()
-
-  method handle_reset_initial why h k =
-    if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
-    (* clear the stack *)
-    while not (Stack.is_empty cmd_stack) do
-      let phrase = Stack.pop cmd_stack in
-      input_buffer#delete_mark phrase.start;
-      input_buffer#delete_mark phrase.stop
-    done;
-    (* reset the buffer *)
-    let start = input_buffer#start_iter in
-    let stop = input_buffer#end_iter in
-    input_buffer#move_mark ~where:start (`NAME "start_of_input");
-    input_buffer#remove_tag Tags.Script.processed ~start ~stop;
-    input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-    input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
-    tag_on_insert (input_buffer :> GText.buffer);
-    (* clear the views *)
-    message_view#clear ();
-    proof_view#clear ();
-    clear_info ();
-    push_info "Restarted";
-    (* apply the initial commands to coq *)
-    self#include_file_dir_in_path h k;
-
-  method include_file_dir_in_path h k =
-    match filename with
-      |None -> k ()
-      |Some f ->
-        let dir = Filename.dirname f in
-        Coq.inloadpath dir h (function
-          |Interface.Fail (_,s) ->
-            self#set_message
-              ("Could not determine lodpath, this might lead to problems:\n"^s);
-            k ()
-          |Interface.Good true |Interface.Unsafe true -> k ()
-          |Interface.Good false |Interface.Unsafe false ->
-            let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-            Coq.interp cmd h (function
-              |Interface.Fail (l,str) ->
-                self#set_message ("Couln't add loadpath:\n"^str);
-                k ()
-              |Interface.Good _ | Interface.Unsafe _ -> k ()))
-
-(** NB: Events during text edition:
-
-    - [begin_user_action]
-    - [insert_text] (or [delete_range] when deleting)
-    - [changed]
-    - [end_user_action]
-
-   When pasting a text containing tags (e.g. the sentence terminators),
-   there is actually many [insert_text] and [changed]. For instance,
-   for "a. b.":
-
-    - [begin_user_action]
-    - [insert_text] (for "a")
-    - [changed]
-    - [insert_text] (for ".")
-    - [changed]
-    - [apply_tag] (for the tag of ".")
-    - [insert_text] (for " b")
-    - [changed]
-    - [insert_text] (for ".")
-    - [changed]
-    - [apply_tag] (for the tag of ".")
-    - [end_user_action]
-
-  Since these copy-pasted tags may interact badly with the retag mechanism,
-  we now don't monitor the "changed" event, but rather the "begin_user_action"
-  and "end_user_action". We begin by setting a mark at the initial cursor
-  point. At the end, the zone between the mark and the cursor is to be
-  untagged and then retagged. *)
-
-  initializer
-  let _ = input_buffer#connect#insert_text
-    ~callback:(fun it s ->
-      (* If a #insert happens in the locked zone, we discard it.
-         Other solution: always use #insert_interactive and similar *)
-      if (it#compare self#get_start_of_input)<0 then
-        GtkSignal.stop_emit ();
-      if String.length s > 1 then
-        let () = Minilib.log "insert_text: Placing cursor" in
-        input_buffer#place_cursor ~where:it;
-        if String.contains s '\n' then
-          let () = Minilib.log "insert_text: Recentering" in
-          self#recenter_insert)
-  in
-  let _ = input_buffer#connect#begin_user_action
-    ~callback:(fun () ->
-      let where = self#get_insert in
-      input_buffer#move_mark (`NAME "prev_insert") ~where;
-      let start = self#get_start_of_input in
-      let stop = input_buffer#end_iter in
-      input_buffer#remove_tag Tags.Script.error ~start ~stop)
-  in
-  let _ = input_buffer#connect#end_user_action
-    ~callback:(fun () ->
-      last_modification_time <- Unix.time ();
-      tag_on_insert (input_buffer :> GText.buffer))
-  in
-  let _ = input_buffer#add_selection_clipboard cb
-  in
-  let _ = input_buffer#connect#after#mark_set
-    ~callback:(fun it m ->
-      !set_location
-        (Printf.sprintf "Line: %5d Char: %3d"
-           (self#get_insert#line + 1)
-           (self#get_insert#line_offset + 1));
-      match GtkText.Mark.get_name m  with
-        | Some "insert" -> ()
-        | Some s -> Minilib.log (s^" moved")
-        | None -> ())
-  in ()
-end
-
-(** [last_make_buf] contains the output of the last make compilation.
-    [last_make] is the same, but as a string, refreshed only when searching
-    the next error.
-*)
-
-let last_make_buf = Buffer.create 1024
-let last_make = ref ""
-let last_make_index = ref 0
-let last_make_dir = ref ""
-let search_compile_error_regexp =
-  Str.regexp
-    "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)"
-
-let search_next_error () =
-  if String.length !last_make <> Buffer.length last_make_buf
-  then last_make := Buffer.contents last_make_buf;
-  let _ =
-    Str.search_forward search_compile_error_regexp !last_make !last_make_index
-  in
-  let f = Str.matched_group 1 !last_make
-  and l = int_of_string (Str.matched_group 2 !last_make)
-  and b = int_of_string (Str.matched_group 3 !last_make)
-  and e = int_of_string (Str.matched_group 4 !last_make)
-  and msg_index = Str.match_beginning ()
-  in
-  last_make_index := Str.group_end 4;
-  (Filename.concat !last_make_dir f, l, b, e,
-   String.sub !last_make msg_index (String.length !last_make - msg_index))
-
-
-(**********************************************************************)
-(* session creation and primitive handling                            *)
-(**********************************************************************)
-
-let create_session file =
-  let basename = match file with
-    |None -> "*scratch*"
-    |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f)
-  in
-  let coqtop_args = match file with
-    |None -> !sup_args
-    |Some the_file ->
-      let get_args f = Project_file.args_from_project f
-        !custom_project_files prefs.project_file_name
-      in
-      match prefs.read_project with
-	|Ignore_args -> !sup_args
-	|Append_args -> get_args the_file @ !sup_args
-	|Subst_args -> get_args the_file
-  in
-  let coqtop = Coq.spawn_coqtop coqtop_args
-  in
-  let buffer = GSourceView2.source_buffer
-    ~tag_table:Tags.Script.table
-    ~highlight_matching_brackets:true
-    ?language:(lang_manager#language prefs.source_language)
-    ?style_scheme:(style_manager#style_scheme prefs.source_style)
-    ()
-  in
-  let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
-  let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
-  let _ = buffer#place_cursor ~where:buffer#start_iter
-  in
-  let script = Wg_ScriptView.script_view coqtop ~source_buffer:buffer
-    ~show_line_numbers:true ~wrap_mode:`NONE ()
-  in
-  let _ = script#misc#set_name "ScriptWindow"
-  in
-  let proof = Wg_ProofView.proof_view () in
-  let _ = proof#misc#set_can_focus true in
-  let _ =
-    GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION]
-  in
-  let message = Wg_MessageView.message_view () in
-  let _ = message#misc#set_can_focus true
-  in
-  let command = new Wg_Command.command_window coqtop in
-  let finder = new Wg_Find.finder (script :> GText.view) in
-  let view = new analyzed_view script proof message coqtop file in
-  let _ = Coq.set_reset_handler coqtop view#handle_reset_initial in
-  let _ = view#update_stats in
-  let _ = Coq.init_coqtop coqtop
-    (fun h k ->
-      view#include_file_dir_in_path h
-        (fun () ->
-          let fold accu (opts, _, _, _, dflt) =
-            List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts
-          in
-          let options = List.fold_left fold [] print_items in
-          Coq.PrintOpt.set options h k))
-  in
-  { tab_label= GMisc.label ~text:basename ();
-    script=script;
-    proof_view=proof;
-    message_view=message;
-    analyzed_view=view;
-    toplvl=coqtop;
-    command=command;
-    finder=finder;
-  }
-
-(*********************************************************************)
-(* functions called by the user interface                            *)
-(*********************************************************************)
-
-(* Nota: using && here has the advantage of working both under win32 and unix.
-   If someday we want the main command to be tried even if the "cd" has failed,
-   then we should use " ; " under unix but " & " under win32 (cf. #2363).
-*)
-
-let local_cd file =
-  "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
-
-let pr_exit_status = function
-  | Unix.WEXITED 0 -> " succeeded"
-  | _ -> " failed"
+let create_session f = Session.create f (make_coqtop_args f) print_items
 
 (** Auxiliary functions for the File operations *)
 
@@ -1049,12 +121,12 @@ let load_file ?(maycreate=false) f =
     let is_f = CUnix.same_file f in
     let rec search_f i = function
       | [] -> false
-      | p :: pages ->
-        match p.analyzed_view#filename with
-	  | Some fn when is_f fn -> session_notebook#goto_page i; true
-          | _ -> search_f (i+1) pages
+      | sn :: sessions ->
+        match sn.fileops#filename with
+	  | Some fn when is_f fn -> notebook#goto_page i; true
+          | _ -> search_f (i+1) sessions
     in
-    if not (search_f 0 session_notebook#pages) then begin
+    if not (search_f 0 notebook#pages) then begin
       Minilib.log "Loading: get raw content";
       let b = Buffer.create 1024 in
       if Sys.file_exists f then Ideutils.read_file f b
@@ -1063,16 +135,16 @@ let load_file ?(maycreate=false) f =
       let s = do_convert (Buffer.contents b) in
       Minilib.log "Loading: create view";
       let session = create_session (Some f) in
-      let index = session_notebook#append_term session in
-      session_notebook#goto_page index;
+      let index = notebook#append_term session in
+      notebook#goto_page index;
       Minilib.log "Loading: stats";
-      session.analyzed_view#update_stats;
-      let input_buffer = session.script#buffer in
+      session.fileops#update_stats;
+      let input_buffer = session.buffer in
       Minilib.log "Loading: fill buffer";
       input_buffer#set_text s;
       input_buffer#set_modified false;
       input_buffer#place_cursor ~where:input_buffer#start_iter;
-      force_retag input_buffer;
+      Sentence.tag_all input_buffer;
       session.script#clear_undo ();
       !refresh_editor_hook ();
       Minilib.log "Loading: success";
@@ -1082,23 +154,22 @@ let load_file ?(maycreate=false) f =
 let confirm_save ok =
   if ok then flash_info "Saved" else warning "Save Failed"
 
-let select_and_save ~saveas ?filename current =
-  let av = current.analyzed_view in
-  let do_save = if saveas then av#save_as else av#save in
+let select_and_save ~saveas ?filename sn =
+  let do_save = if saveas then sn.fileops#saveas else sn.fileops#save in
   let title = if saveas then "Save file as" else "Save file" in
   match select_file_for_save ~title ?filename () with
     |None -> false
     |Some f ->
       let ok = do_save f in
       confirm_save ok;
-      if ok then current.tab_label#set_text (Filename.basename f);
+      if ok then sn.tab_label#set_text (Filename.basename f);
       ok
 
-let check_save ~saveas current =
-  try match current.analyzed_view#filename with
-    |None -> select_and_save ~saveas current
+let check_save ~saveas sn =
+  try match sn.fileops#filename with
+    |None -> select_and_save ~saveas sn
     |Some f ->
-      let ok = current.analyzed_view#save f in
+      let ok = sn.fileops#save f in
       confirm_save ok;
       ok
   with _ -> warning "Save Failed"; false
@@ -1107,14 +178,14 @@ exception DontQuit
 
 let check_quit saveall =
   (try save_pref () with _ -> flash_info "Cannot save preferences");
-  let is_modified p = p.script#buffer#modified in
-  if List.exists is_modified session_notebook#pages then begin
+  let is_modified sn = sn.buffer#modified in
+  if List.exists is_modified notebook#pages then begin
     let answ = GToolbox.question_box ~title:"Quit"
       ~buttons:["Save Named Buffers and Quit";
                 "Quit without Saving";
                 "Don't Quit"]
       ~default:0
-      ~icon:warn_image
+      ~icon:warn_image#coerce
       "There are unsaved buffers"
     in
     match answ with
@@ -1122,11 +193,11 @@ let check_quit saveall =
       | 2 -> ()
       | _ -> raise DontQuit
   end;
-  List.iter (fun p -> Coq.close_coqtop p.toplvl) session_notebook#pages
+  List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages
 
 (* For MacOS, just to be sure, we close all coqtops (again?) *)
 let close_and_quit () =
-  List.iter (fun p -> Coq.close_coqtop p.toplvl) session_notebook#pages;
+  List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages;
   Coq.final_countdown ()
 
 let crash_save exitcode =
@@ -1135,18 +206,18 @@ let crash_save exitcode =
     let r = ref 0 in
     fun () -> incr r; string_of_int !r
   in
-  let save_page p =
-    let filename = match p.analyzed_view#filename with
+  let save_session sn =
+    let filename = match sn.fileops#filename with
       | None -> "Unnamed_coqscript_" ^ idx () ^ ".crashcoqide"
       | Some f -> f^".crashcoqide"
     in
     try
-      if try_export filename (p.script#buffer#get_text ()) then
+      if try_export filename (sn.buffer#get_text ()) then
 	Minilib.log ("Saved "^filename)
       else Minilib.log ("Could not save "^filename)
     with _ -> Minilib.log ("Could not save "^filename)
   in
-  List.iter save_page session_notebook#pages;
+  List.iter save_session notebook#pages;
   Minilib.log "End emergency save";
   exit exitcode
 
@@ -1158,9 +229,9 @@ module File = struct
 
 let newfile _ =
   let session = create_session None in
-  let index = session_notebook#append_term session in
+  let index = notebook#append_term session in
   !refresh_editor_hook ();
-  session_notebook#goto_page index
+  notebook#goto_page index
 
 let load _ =
   match select_file_for_open ~title:"Load file" () with
@@ -1168,27 +239,26 @@ let load _ =
     | Some f -> FileAux.load_file f
 
 let save _ =
-  ignore (FileAux.check_save ~saveas:false session_notebook#current_term)
+  ignore (FileAux.check_save ~saveas:false notebook#current_term)
 
 let saveas _ =
-  let current = session_notebook#current_term in
+  let sn = notebook#current_term in
   try
-    let filename = current.analyzed_view#filename in
-    ignore (FileAux.select_and_save ~saveas:true ?filename current)
+    let filename = sn.fileops#filename in
+    ignore (FileAux.select_and_save ~saveas:true ?filename sn)
   with _ -> warning "Save Failed"
 
 let saveall _ =
   List.iter
-    (function {analyzed_view = av} -> match av#filename with
+    (fun sn -> match sn.fileops#filename with
       | None -> ()
-      | Some f -> ignore (av#save f))
-    session_notebook#pages
+      | Some f -> ignore (sn.fileops#save f))
+    notebook#pages
 
 let revert_all _ =
   List.iter
-    (function {analyzed_view = av} ->
-      if av#changed_on_disk then av#revert)
-    session_notebook#pages
+    (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)
+    notebook#pages
 
 let quit _ =
   try FileAux.check_quit saveall; Coq.final_countdown ()
@@ -1196,27 +266,27 @@ let quit _ =
 
 let close_buffer _ =
   let do_remove () =
-    session_notebook#remove_page session_notebook#current_page
+    notebook#remove_page notebook#current_page
   in
-  let current = session_notebook#current_term in
-  if not current.script#buffer#modified then do_remove ()
+  let sn = notebook#current_term in
+  if not sn.buffer#modified then do_remove ()
   else
     let answ = GToolbox.question_box ~title:"Close"
       ~buttons:["Save Buffer and Close";
                 "Close without Saving";
                 "Don't Close"]
       ~default:0
-      ~icon:warn_image
+      ~icon:warn_image#coerce
       "This buffer has unsaved modifications"
     in
     match answ with
-      | 1 when FileAux.check_save ~saveas:true current -> do_remove ()
+      | 1 when FileAux.check_save ~saveas:true sn -> do_remove ()
       | 2 -> do_remove ()
       | _ -> ()
 
 let export kind _ =
-  let av = current_view () in
-  match av#filename with
+  let sn = notebook#current_term in
+  match sn.fileops#filename with
     |None -> flash_info "Cannot print: this buffer has no name"
     |Some f ->
       let basef = Filename.basename f in
@@ -1231,14 +301,14 @@ let export kind _ =
         local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      av#set_message ("Running: "^cmd);
+      sn.messages#set ("Running: "^cmd);
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
-      run_command av#insert_message finally cmd
+      run_command sn.messages#add finally cmd
 
 let print _ =
-  let av = current_view () in
-  match av#filename with
+  let sn = notebook#current_term in
+  match sn.fileops#filename with
     |None -> flash_info "Cannot print: this buffer has no name"
     |Some f_name ->
       let cmd =
@@ -1273,27 +343,27 @@ let print _ =
       w#misc#show ()
 
 let highlight _ =
-  let trm = session_notebook#current_term in
-  force_retag trm.script#buffer;
-  trm.analyzed_view#recenter_insert
+  let sn = notebook#current_term in
+  Sentence.tag_all sn.buffer;
+  sn.script#recenter_insert
 
 end
 
 (** Timers *)
 
 let reset_revert_timer () =
-  revert_timer.kill ();
+  FileOps.revert_timer.kill ();
   if prefs.global_auto_revert then
-    revert_timer.run
+    FileOps.revert_timer.run
       ~ms:prefs.global_auto_revert_delay
       ~callback:(fun () -> File.revert_all (); true)
 
 let reset_autosave_timer () =
-  let autosave p = try p.analyzed_view#auto_save with _ -> () in
-  let autosave_all () = List.iter autosave session_notebook#pages; true in
-  autosave_timer.kill ();
+  let autosave sn = try sn.fileops#auto_save with _ -> () in
+  let autosave_all () = List.iter autosave notebook#pages; true in
+  FileOps.autosave_timer.kill ();
   if prefs.auto_save then
-    autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all
+    FileOps.autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all
 
 (** Export of functions used in [coqide_main] : *)
 
@@ -1309,20 +379,39 @@ let do_load f = FileAux.load_file f
 
 module External = struct
 
+let coq_makefile _ =
+  let sn = notebook#current_term in
+  match sn.fileops#filename with
+    |None -> flash_info "Cannot make makefile: this buffer has no name"
+    |Some f ->
+      let cmd = local_cd f ^ prefs.cmd_coqmakefile in
+      let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st)
+      in
+      run_command ignore finally cmd
+
+let editor _ =
+  let sn = notebook#current_term in
+  match sn.fileops#filename with
+    |None -> warning "Call to external editor available only on named files"
+    |Some f ->
+      File.save ();
+      let f = Filename.quote f in
+      let cmd = Util.subst_command_placeholder prefs.cmd_editor f in
+      run_command ignore (fun _ -> sn.fileops#revert) cmd
+
 let compile _ =
-  let v = session_notebook#current_term in
-  let av = v.analyzed_view in
+  let sn = notebook#current_term in
   File.save ();
-  match av#filename with
+  match sn.fileops#filename with
     |None -> flash_info "Active buffer has no name"
     |Some f ->
       let cmd = prefs.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f))
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      av#set_message ("Running: "^cmd);
+      sn.messages#set ("Running: "^cmd);
       let display s =
-        av#insert_message s;
+        sn.messages#add s;
         Buffer.add_string buf s
       in
       let finally st =
@@ -1330,68 +419,76 @@ let compile _ =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          av#set_message "Compilation output:\n";
-          av#insert_message (Buffer.contents buf);
+          sn.messages#set "Compilation output:\n";
+          sn.messages#add (Buffer.contents buf);
         end
       in
       run_command display finally cmd
 
+(** [last_make_buf] contains the output of the last make compilation.
+    [last_make] is the same, but as a string, refreshed only when searching
+    the next error. *)
+
+let last_make_buf = Buffer.create 1024
+let last_make = ref ""
+let last_make_index = ref 0
+let last_make_dir = ref ""
+
 let make _ =
-  let av = current_view () in
-  match av#filename with
+  let sn = notebook#current_term in
+  match sn.fileops#filename with
     |None -> flash_info "Cannot make: this buffer has no name"
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ prefs.cmd_make ^ " 2>&1" in
-      av#set_message "Compilation output:\n";
+      sn.messages#set "Compilation output:\n";
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
       last_make_dir := Filename.dirname f;
       let display s =
-        av#insert_message s;
+        sn.messages#add s;
         Buffer.add_string last_make_buf s
       in
       let finally st = flash_info (current.cmd_make ^ pr_exit_status st)
       in
       run_command display finally cmd
 
+let search_compile_error_regexp =
+  Str.regexp
+    "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)"
+
+let search_next_error () =
+  if String.length !last_make <> Buffer.length last_make_buf
+  then last_make := Buffer.contents last_make_buf;
+  let _ =
+    Str.search_forward search_compile_error_regexp !last_make !last_make_index
+  in
+  let f = Str.matched_group 1 !last_make
+  and l = int_of_string (Str.matched_group 2 !last_make)
+  and b = int_of_string (Str.matched_group 3 !last_make)
+  and e = int_of_string (Str.matched_group 4 !last_make)
+  and msg_index = Str.match_beginning ()
+  in
+  last_make_index := Str.group_end 4;
+  (Filename.concat !last_make_dir f, l, b, e,
+   String.sub !last_make msg_index (String.length !last_make - msg_index))
+
 let next_error _ =
   try
     let file,line,start,stop,error_msg = search_next_error () in
     FileAux.load_file file;
-    let v = session_notebook#current_term in
-    let av = v.analyzed_view in
-    let input_buffer = v.script#buffer in
-    let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
-    let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
-    input_buffer#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
-    input_buffer#place_cursor ~where:starti;
-    av#set_message error_msg;
-    v.script#misc#grab_focus ()
+    let sn = notebook#current_term in
+    let b = sn.buffer in
+    let starti = b#get_iter_at_byte ~line:(line-1) start in
+    let stopi = b#get_iter_at_byte ~line:(line-1) stop in
+    b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
+    b#place_cursor ~where:starti;
+    sn.messages#set error_msg;
+    sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    (current_view ())#set_message "No more errors.\n"
-
-let coq_makefile _ =
-  let av = current_view () in
-  match av#filename with
-    |None -> flash_info "Cannot make makefile: this buffer has no name"
-    |Some f ->
-      let cmd = local_cd f ^ prefs.cmd_coqmakefile in
-      let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st)
-      in
-      run_command ignore finally cmd
-
-let editor _ =
-  let av = current_view () in
-  match av#filename with
-    |None -> warning "Call to external editor available only on named files"
-    |Some f ->
-      File.save ();
-      let f = Filename.quote f in
-      let cmd = Util.subst_command_placeholder prefs.cmd_editor f in
-      run_command ignore (fun _ -> av#revert) cmd
+    notebook#current_term.messages#set "No more errors.\n"
 
 end
 
@@ -1414,35 +511,64 @@ let update_status h k =
       in
       display ("Ready" ^ path ^ name); k ())
 
+let find_next_occurrence ~backward =
+  (** go to the next occurrence of the current word, forward or backward *)
+  let sn = notebook#current_term in
+  let b = sn.buffer in
+  let start = find_word_start (b#get_iter_at_mark `INSERT) in
+  let stop = find_word_end start in
+  let text = b#get_text ~start ~stop () in
+  let search = if backward then start#backward_search else stop#forward_search
+  in
+  match search text with
+    |None -> ()
+    |Some(where, _) -> b#place_cursor ~where; sn.script#recenter_insert
+
 let send_to_coq f =
-  let term = session_notebook#current_term in
-  let av = term.analyzed_view in
+  let sn = notebook#current_term in
   let info () = Minilib.log ("Coq busy, discarding query") in
-  let f h k = f av h (fun () -> update_status h k) in
-  Coq.try_grab term.toplvl f info
+  let f h k = f sn h (fun () -> update_status h k) in
+  Coq.try_grab sn.coqtop f info
 
 module Nav = struct
-  let forward_one _ = send_to_coq (fun a -> a#process_next_phrase)
-  let backward_one _ = send_to_coq (fun a -> a#backtrack_last_phrase)
-  let goto _ = send_to_coq (fun a -> a#go_to_insert)
-  let restart _ = force_reset_initial ()
-  let goto_end _ = send_to_coq (fun a -> a#process_until_end_or_error)
-  let interrupt _ = break ()
-  let previous_occ _ = (current_view ())#find_next_occurrence Up
-  let next_occ _ = (current_view ())#find_next_occurrence Down
+  let forward_one _ = send_to_coq (fun sn -> sn.coqops#process_next_phrase)
+  let backward_one _ = send_to_coq (fun sn -> sn.coqops#backtrack_last_phrase)
+  let goto _ = send_to_coq (fun sn -> sn.coqops#go_to_insert)
+  let goto_end _ = send_to_coq (fun sn -> sn.coqops#process_until_end_or_error)
+  let previous_occ _ = find_next_occurrence ~backward:true
+  let next_occ _ = find_next_occurrence ~backward:false
+  let restart _ =
+    Minilib.log "Reset Initial";
+    Coq.reset_coqtop notebook#current_term.coqtop
+  let interrupt _ =
+    Minilib.log "User break received";
+    Coq.break_coqtop notebook#current_term.coqtop
 end
 
-let tactic_wizard_callback l _ = send_to_coq (fun a -> a#tactic_wizard l)
+let tactic_wizard_callback l _ =
+  send_to_coq (fun sn -> sn.coqops#tactic_wizard l)
 
 let printopts_callback opts v =
   let b = v#get_active in
   let opts = List.map (fun o -> (o,b)) opts in
-  send_to_coq (fun av h k ->
+  send_to_coq (fun sn h k ->
     Coq.PrintOpt.set opts h
-      (fun () -> av#show_goals h k))
+      (fun () -> sn.coqops#show_goals h k))
 
 (** Templates menu *)
 
+let get_current_word () = match Ideutils.cb#text with
+  |Some t -> Minilib.log ("get_current_word : selection = " ^ t); t
+  |None ->
+    Minilib.log "get_current_word : none selected";
+    let b = current_buffer () in
+    let it = b#get_iter_at_mark `INSERT in
+    let start = find_word_start it in
+    let stop = find_word_end start in
+    b#move_mark `SEL_BOUND ~where:start;
+    b#move_mark `INSERT ~where:stop;
+    b#get_text ~slice:true ~start ~stop ()
+
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
     (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
@@ -1474,7 +600,7 @@ let display_match k = function
 
 let match_callback _ =
   let w = get_current_word () in
-  let coqtop = session_notebook#current_term.toplvl in
+  let coqtop = notebook#current_term.coqtop in
   Coq.try_grab coqtop (fun h k -> Coq.mkcases w h (display_match k)) ignore
 
 (** Queries *)
@@ -1483,8 +609,8 @@ module Query = struct
 
 let searchabout () =
   let word = get_current_word () in
-  let term = session_notebook#current_term in
-  let buf = term.message_view#buffer in
+  let sn = notebook#current_term in
+  let buf = sn.messages#buffer in
   let insert result =
     let qualid = result.Interface.coq_object_qualid in
     let name = String.concat "." qualid in
@@ -1495,22 +621,22 @@ let searchabout () =
     buf#insert "\n";
   in
   let display_results k r =
-    term.message_view#clear ();
+    sn.messages#clear;
     List.iter insert (match r with Interface.Good l -> l | _ -> []);
     k ()
   in
   let launch_query h k =
     Coq.search [Interface.SubType_Pattern word, true] h (display_results k)
   in
-  Coq.try_grab term.toplvl launch_query ignore
+  Coq.try_grab sn.coqtop launch_query ignore
 
 let otherquery command _ =
   let word = get_current_word () in
-  let term = session_notebook#current_term in
+  let sn = notebook#current_term in
   if word <> "" then
     let query = command ^ " " ^ word ^ "." in
-    term.message_view#clear ();
-    Coq.try_grab term.toplvl (term.analyzed_view#raw_coq_query query) ignore
+    sn.messages#clear;
+    Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
 let query command _ =
   if command = "SearchAbout"
@@ -1525,8 +651,8 @@ module MiscMenu = struct
 
 let detach_view _ =
   (* Open a separate window containing the current buffer *)
-  let trm = session_notebook#current_term in
-  let file = match trm.analyzed_view#filename with
+  let sn = notebook#current_term in
+  let file = match sn.fileops#filename with
     |None -> "*scratch*"
     |Some f -> f
   in
@@ -1537,11 +663,11 @@ let detach_view _ =
   in
   let sb = GBin.scrolled_window ~packing:w#add ()
   in
-  let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add ()
+  let nv = GText.view ~buffer:sn.buffer ~packing:sb#add ()
   in
   nv#misc#modify_font prefs.text_font;
   (* If the buffer in the main window is closed, destroy this detached view *)
-  ignore (trm.script#connect#destroy ~callback:w#destroy)
+  ignore (sn.script#connect#destroy ~callback:w#destroy)
 
 let log_file_message () =
   if !Minilib.debug then
@@ -1560,7 +686,7 @@ let initial_about () =
     else ""
   in
   let msg = initial_string ^ version_info ^ log_file_message () in
-  session_notebook#current_term.message_view#push Interface.Notice msg
+  notebook#current_term.messages#add msg
 
 let coq_icon () =
   (* May raise Nof_found *)
@@ -1598,8 +724,8 @@ let about _ =
   dialog#set_authors authors;
   dialog#show ()
 
-  let comment _ = session_notebook#current_term.script#comment ()
-  let uncomment _ = session_notebook#current_term.script#uncomment ()
+  let comment _ = notebook#current_term.script#comment ()
+  let uncomment _ = notebook#current_term.script#uncomment ()
 
 end
 
@@ -1614,39 +740,47 @@ let refresh_editor_prefs () =
   let fd = prefs.text_font in
   let clr = Tags.color_of_string prefs.background_color
   in
-  let iter_page p =
+  let iter_session sn =
     (* Editor settings *)
-    p.script#set_wrap_mode wrap_mode;
-    p.script#set_show_line_numbers prefs.show_line_number;
-    p.script#set_auto_indent prefs.auto_indent;
-    p.script#set_highlight_current_line prefs.highlight_current_line;
+    sn.script#set_wrap_mode wrap_mode;
+    sn.script#set_show_line_numbers prefs.show_line_number;
+    sn.script#set_auto_indent prefs.auto_indent;
+    sn.script#set_highlight_current_line prefs.highlight_current_line;
 
     (* Hack to handle missing binding in lablgtk *)
     let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int }
     in
-    Gobject.set conv p.script#as_widget show_spaces;
+    Gobject.set conv sn.script#as_widget show_spaces;
 
-    p.script#set_show_right_margin prefs.show_right_margin;
-    p.script#set_insert_spaces_instead_of_tabs
+    sn.script#set_show_right_margin prefs.show_right_margin;
+    sn.script#set_insert_spaces_instead_of_tabs
       prefs.spaces_instead_of_tabs;
-    p.script#set_tab_width prefs.tab_length;
-    p.script#set_auto_complete prefs.auto_complete;
+    sn.script#set_tab_width prefs.tab_length;
+    sn.script#set_auto_complete prefs.auto_complete;
 
     (* Fonts *)
-    p.script#misc#modify_font fd;
-    p.proof_view#misc#modify_font fd;
-    p.message_view#misc#modify_font fd;
-    p.command#refresh_font ();
+    sn.script#misc#modify_font fd;
+    sn.proof#misc#modify_font fd;
+    sn.messages#misc#modify_font fd;
+    sn.command#refresh_font ();
 
     (* Colors *)
-    p.script#misc#modify_base [`NORMAL, `COLOR clr];
-    p.proof_view#misc#modify_base [`NORMAL, `COLOR clr];
-    p.message_view#misc#modify_base [`NORMAL, `COLOR clr];
-    p.command#refresh_color ()
+    sn.script#misc#modify_base [`NORMAL, `COLOR clr];
+    sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
+    sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
+    sn.command#refresh_color ()
 
   in
-  List.iter iter_page session_notebook#pages
+  List.iter iter_session notebook#pages
 
+let refresh_notebook_pos () =
+  let pos = match prefs.vertical_tabs, prefs.opposite_tabs with
+    | false, false -> `TOP
+    | false, true  -> `BOTTOM
+    | true , false -> `LEFT
+    | true , true  -> `RIGHT
+  in
+  notebook#set_tab_pos pos
 
 (** Wrappers around GAction functions for creating menus *)
 
@@ -1723,7 +857,9 @@ let emit_to_focus window sgn =
   let obj = Gobject.unsafe_cast focussed_widget in
   try GtkSignal.emit_unit obj ~sgn with _ -> ()
 
-(** Creation of the main coqide window *)
+
+
+(** {2 Creation of the main coqide window } *)
 
 let build_ui () =
   let w = GWindow.window
@@ -1783,9 +919,9 @@ let build_ui () =
   menu edit_menu [
     item "Edit" ~label:"_Edit";
     item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO
-      ~callback:(fun _ -> session_notebook#current_term.script#undo ());
+      ~callback:(fun _ -> notebook#current_term.script#undo ());
     item "Redo" ~stock:`REDO
-      ~callback:(fun _ -> session_notebook#current_term.script#redo ());
+      ~callback:(fun _ -> notebook#current_term.script#redo ());
     item "Cut" ~stock:`CUT
       ~callback:(fun _ -> emit_to_focus w GtkText.View.S.cut_clipboard);
     item "Copy" ~stock:`COPY
@@ -1793,20 +929,20 @@ let build_ui () =
     item "Paste" ~stock:`PASTE
       ~callback:(fun _ -> emit_to_focus w GtkText.View.S.paste_clipboard);
     item "Find" ~stock:`FIND
-      ~callback:(fun _ -> session_notebook#current_term.finder#show `FIND);
+      ~callback:(fun _ -> notebook#current_term.finder#show `FIND);
     item "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
-      ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ());
+      ~callback:(fun _ -> notebook#current_term.finder#find_forward ());
     item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
       ~accel:"<Shift>F3"
-      ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ());
+      ~callback:(fun _ -> notebook#current_term.finder#find_backward ());
     item "Replace" ~stock:`FIND_AND_REPLACE
-      ~callback:(fun _ -> session_notebook#current_term.finder#show `REPLACE);
+      ~callback:(fun _ -> notebook#current_term.finder#show `REPLACE);
     item "Close Find" ~accel:"Escape"
-      ~callback:(fun _ -> session_notebook#current_term.finder#hide ());
+      ~callback:(fun _ -> notebook#current_term.finder#hide ());
     item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
       ~callback:(fun _ ->
         ignore ( ()
-(*	       let av = session_notebook#current_term.analyzed_view in
+(*	       let av = notebook#current_term.analyzed_view in
 	       av#complete_at_offset (av#get_insert)#offset*)
 	));
     item "External editor" ~label:"External editor" ~stock:`EDIT
@@ -1814,7 +950,7 @@ let build_ui () =
     item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
       ~callback:(fun _ ->
         begin
-	  try configure ~apply:update_notebook_pos ()
+	  try Preferences.configure ~apply:refresh_notebook_pos ()
 	  with _ -> flash_info "Cannot save preferences"
         end;
         reset_revert_timer ());
@@ -1824,10 +960,10 @@ let build_ui () =
     item "View" ~label:"_View";
     item "Previous tab" ~label:"_Previous tab" ~accel:"<Alt>Left"
       ~stock:`GO_BACK
-      ~callback:(fun _ -> session_notebook#previous_page ());
+      ~callback:(fun _ -> notebook#previous_page ());
     item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right"
       ~stock:`GO_FORWARD
-      ~callback:(fun _ -> session_notebook#next_page ());
+      ~callback:(fun _ -> notebook#next_page ());
     toggle_item "Show Toolbar" ~label:"Show _Toolbar"
       ~active:(prefs.show_toolbar)
       ~callback:(fun _ ->
@@ -1836,7 +972,7 @@ let build_ui () =
     toggle_item "Show Query Pane" ~label:"Show _Query Pane"
       ~accel:"<Alt>Escape"
       ~callback:(fun _ ->
-        let ccw = session_notebook#current_term.command in
+        let ccw = notebook#current_term.command in
         if ccw#frame#misc#visible
         then ccw#frame#misc#hide ()
         else ccw#frame#misc#show ())
@@ -1865,8 +1001,8 @@ let build_ui () =
       ~accel:(prefs.modifier_for_navigation^"Break");
 (* wait for this available in GtkSourceView !
       item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
-	~callback:(fun _ -> let sess = session_notebook#current_term in
-		     toggle_proof_visibility sess.script#buffer
+	~callback:(fun _ -> let sess = notebook#current_term in
+		     toggle_proof_visibility sess.buffer
 		       sess.analyzed_view#get_insert) ~tooltip:"Hide proof"
 	~accel:(prefs.modifier_for_navigation^"h");*)
     item "Previous" ~label:"_Previous" ~stock:`GO_BACK
@@ -1953,16 +1089,13 @@ let build_ui () =
     item "Help" ~label:"_Help";
     item "Browse Coq Manual" ~label:"Browse Coq _Manual"
       ~callback:(fun _ ->
-	let av = session_notebook#current_term.analyzed_view in
-	browse av#insert_message (doc_url ()));
+        browse notebook#current_term.messages#add (doc_url ()));
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-	let av = session_notebook#current_term.analyzed_view in
-	browse av#insert_message prefs.library_url);
+        browse notebook#current_term.messages#add prefs.library_url);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ ->
-        let av = session_notebook#current_term.analyzed_view in
-	av#help_for_keyword ());
+        browse_keyword notebook#current_term.messages#add (get_current_word ()));
     item "About Coq" ~label:"_About" ~stock:`ABOUT
       ~callback:MiscMenu.about
   ];
@@ -1996,13 +1129,13 @@ let build_ui () =
   let () = vbox#pack toolbar in
 
   (* Reset on tab switch *)
-  let _ = session_notebook#connect#switch_page ~callback:(fun _ ->
-    if prefs.reset_on_tab_switch then force_reset_initial ())
+  let _ = notebook#connect#switch_page ~callback:(fun _ ->
+    if prefs.reset_on_tab_switch then Nav.restart ())
   in
 
   (* Vertical Separator between Scripts and Goals *)
-  let () = vbox#pack ~expand:true session_notebook#coerce in
-  let () = update_notebook_pos () in
+  let () = vbox#pack ~expand:true notebook#coerce in
+  let () = refresh_notebook_pos () in
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let () = lower_hbox#pack ~expand:true status#coerce in
   let () = push_info "Ready" in
@@ -2020,7 +1153,7 @@ let build_ui () =
   let () = lower_hbox#pack pbar#coerce in
   let () = pbar#set_text "CoqIde started" in
   let _ = Glib.Timeout.add ~ms:300 ~callback:(fun () ->
-    let curr_coq = session_notebook#current_term.toplvl in
+    let curr_coq = notebook#current_term.coqtop in
     if Coq.is_computing curr_coq then pbar#pulse ();
     true)
   in
@@ -2033,8 +1166,8 @@ let build_ui () =
   in
   let refresh_style () =
     let style =  style_manager#style_scheme prefs.source_style in
-    let iter_page p = p.script#source_buffer#set_style_scheme style in
-    List.iter iter_page session_notebook#pages
+    let iter_session v = v.script#source_buffer#set_style_scheme style in
+    List.iter iter_session notebook#pages
   in
   let resize_window () =
     w#resize ~width:prefs.window_width ~height:prefs.window_height
@@ -2044,7 +1177,7 @@ let build_ui () =
   refresh_style_hook := refresh_style;
   refresh_editor_hook := refresh_editor_prefs;
   resize_window_hook := resize_window;
-  refresh_tabs_hook := update_notebook_pos;
+  refresh_tabs_hook := refresh_notebook_pos;
 
   (* Color configuration *)
   Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
@@ -2053,6 +1186,9 @@ let build_ui () =
   (* Showtime ! *)
   w#show ()
 
+
+(** {2 Coqide main function } *)
+
 let make_file_buffer f =
   let f =
     if Sys.file_exists f || Filename.check_suffix f ".v" then f
@@ -2062,7 +1198,7 @@ let make_file_buffer f =
 
 let make_scratch_buffer () =
   let session = create_session None in
-  let _ = session_notebook#append_term session in
+  let _ = notebook#append_term session in
   !refresh_editor_hook ()
 
 let main files =
@@ -2072,13 +1208,16 @@ let main files =
   (match files with
     | [] -> make_scratch_buffer ()
     | _ -> List.iter make_file_buffer files);
-  session_notebook#goto_page 0;
+  notebook#goto_page 0;
   MiscMenu.initial_about ();
-  session_notebook#current_term.script#misc#grab_focus ();
+  notebook#current_term.script#misc#grab_focus ();
   Minilib.log "End of Coqide.main"
 
-(* This function check every tenth of second if GeoProof has send
-   something on his private clipboard *)
+
+(** {2 Geoproof } *)
+
+(** This function check every tenth of second if GeoProof has send
+    something on his private clipboard *)
 
 let check_for_geoproof_input () =
   let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
@@ -2093,6 +1232,9 @@ let check_for_geoproof_input () =
   in
   ignore (GMain.Timeout.add ~ms:100 ~callback:handler)
 
+
+(** {2 Argument parsing } *)
+
 (** By default, the coqtop we try to launch is exactly the current coqide
     full name, with the last occurrence of "coqide" replaced by "coqtop".
     This should correctly handle the ".opt", ".byte", ".exe" situations.
@@ -2124,7 +1266,8 @@ let read_coqide_args argv =
   custom_project_files := project_files;
   argv
 
-(** * Coqide's handling of signals *)
+
+(** {2 Signal handling } *)
 
 (** The Ctrl-C (sigint) is handled as a interactive quit.
     For most of the other catchable signals we launch
diff --git a/ide/fileOps.ml b/ide/fileOps.ml
new file mode 100644
index 000000000..a1066db2c
--- /dev/null
+++ b/ide/fileOps.ml
@@ -0,0 +1,154 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Ideutils
+
+let prefs = Preferences.current
+
+let revert_timer = mktimer ()
+let autosave_timer = mktimer ()
+
+class type ops =
+object
+  method filename : string option
+  method update_stats : unit
+  method changed_on_disk : bool
+  method revert : unit
+  method auto_save : unit
+  method save : string -> bool
+  method saveas : string -> bool
+end
+
+class fileops (buffer:GText.buffer) _fn (reset_handler:unit->unit) =
+object(self)
+
+  val mutable filename = _fn
+  val mutable last_stats = NoSuchFile
+  val mutable last_modification_time = 0.
+  val mutable last_auto_save_time = 0.
+
+  method filename = filename
+
+  method update_stats = match filename with
+    |Some f -> last_stats <- Ideutils.stat f
+    |_ -> ()
+
+  method changed_on_disk = match filename with
+    |None -> false
+    |Some f -> match Ideutils.stat f, last_stats with
+        |MTime cur_mt, MTime last_mt -> cur_mt > last_mt
+        |MTime _, (NoSuchFile|OtherError) -> true
+        |NoSuchFile, MTime _ ->
+          flash_info ("Warning, file not on disk anymore : "^f);
+          false
+        |_ -> false
+
+  method revert =
+    let do_revert f =
+      push_info "Reverting buffer";
+      try
+        reset_handler ();
+        let b = Buffer.create 1024 in
+        Ideutils.read_file f b;
+        let s = try_convert (Buffer.contents b) in
+        buffer#set_text s;
+        self#update_stats;
+        buffer#place_cursor ~where:buffer#start_iter;
+        buffer#set_modified false;
+        pop_info ();
+        flash_info "Buffer reverted";
+        Sentence.tag_all buffer;
+      with _  ->
+        pop_info ();
+        flash_info "Warning: could not revert buffer";
+    in
+    match filename with
+      | None -> ()
+      | Some f ->
+        if not buffer#modified then do_revert f
+        else
+          let answ = GToolbox.question_box
+            ~title:"Modified buffer changed on disk"
+            ~buttons:["Revert from File";
+                      "Overwrite File";
+                      "Disable Auto Revert"]
+            ~default:0
+            ~icon:(stock_to_widget `DIALOG_WARNING)
+            "Some unsaved buffers changed on disk"
+          in
+          match answ with
+            | 1 -> do_revert f
+            | 2 -> if self#save f then flash_info "Overwritten" else
+                flash_info "Could not overwrite file"
+            | _ ->
+              Minilib.log "Auto revert set to false";
+              prefs.Preferences.global_auto_revert <- false;
+              revert_timer.kill ()
+
+  method save f =
+    if try_export f (buffer#get_text ()) then begin
+      filename <- Some f;
+      self#update_stats;
+      buffer#set_modified false;
+      (match self#auto_save_name with
+        | None -> ()
+        | Some fn -> try Sys.remove fn with _ -> ());
+      true
+    end
+    else false
+
+  method saveas f =
+  if not (Sys.file_exists f) then self#save f
+  else
+    let answ = GToolbox.question_box ~title:"File exists on disk"
+      ~buttons:["Overwrite"; "Cancel";]
+      ~default:1
+      ~icon:warn_image#coerce
+      ("File "^f^" already exists")
+    in
+    match answ with
+      | 1 -> self#save f
+      | _ -> false
+
+  method private auto_save_name =
+    match filename with
+      | None -> None
+      | Some f ->
+        let dir = Filename.dirname f in
+        let base = (fst prefs.Preferences.auto_save_name) ^
+          (Filename.basename f) ^
+          (snd prefs.Preferences.auto_save_name)
+        in Some (Filename.concat dir base)
+
+  method private need_auto_save =
+    buffer#modified &&
+      last_modification_time > last_auto_save_time
+
+  method auto_save =
+    if self#need_auto_save then begin
+      match self#auto_save_name with
+        | None -> ()
+        | Some fn ->
+          try
+            last_auto_save_time <- Unix.time();
+            Minilib.log ("Autosave time: "^(string_of_float (Unix.time())));
+            if try_export fn (buffer#get_text ()) then begin
+              flash_info ~delay:1000 "Autosaved"
+            end
+            else warning
+              ("Autosave failed (check if " ^ fn ^ " is writable)")
+          with _ ->
+            warning ("Autosave: unexpected error while writing "^fn)
+    end
+
+  initializer
+  let _ = buffer#connect#end_user_action
+    ~callback:(fun () -> last_modification_time <- Unix.time ())
+  in ()
+
+end
diff --git a/ide/fileOps.mli b/ide/fileOps.mli
new file mode 100644
index 000000000..bcfae11bd
--- /dev/null
+++ b/ide/fileOps.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+val revert_timer : Ideutils.timer
+val autosave_timer : Ideutils.timer
+
+class type ops =
+object
+  method filename : string option
+  method update_stats : unit
+  method changed_on_disk : bool
+  method revert : unit
+  method auto_save : unit
+  method save : string -> bool
+  method saveas : string -> bool
+end
+
+class fileops : GText.buffer -> string option -> (unit -> unit) -> ops
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 1c3b7f21e..5df0a46ae 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -16,13 +16,17 @@ Preferences
 Project_file
 Ideutils
 Coq
+Coq_lex
+Sentence
 Gtk_parsing
 Wg_ProofView
 Wg_MessageView
 Wg_Find
 Wg_ScriptView
-Coq_lex
 Coq_commands
 Wg_Command
+FileOps
+CoqOps
+Session
 Coqide_ui
 Coqide
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 35a5a2477..ed07135b5 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -11,6 +11,17 @@ open Preferences
 
 exception Forbidden
 
+let warn_image =
+  let img = GMisc.image () in
+  img#set_stock `DIALOG_WARNING;
+  img#set_icon_size `DIALOG;
+  img
+
+let warning msg =
+  GToolbox.message_box ~title:"Warning" ~icon:warn_image#coerce msg
+
+let cb = GData.clipboard Gdk.Atom.primary
+
 (* status bar and locations *)
 
 let status = GMisc.statusbar ()
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 2598dee33..87ddb2a95 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,6 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+val warn_image : GMisc.image
+val warning : string -> unit
+
+val cb : GData.clipboard
+
 val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
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
diff --git a/ide/sentence.mli b/ide/sentence.mli
new file mode 100644
index 000000000..c552024f4
--- /dev/null
+++ b/ide/sentence.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Retag the ends of sentences around an inserted zone *)
+
+val tag_on_insert : GText.buffer -> unit
+
+(** Retag the ends of sentences in the whole buffer *)
+
+val tag_all : GText.buffer -> unit
+
+(** Search a sentence around some position *)
+
+val find : GText.buffer -> GText.iter -> (GText.iter * GText.iter) option
diff --git a/ide/session.ml b/ide/session.ml
new file mode 100644
index 000000000..ac23e2f0a
--- /dev/null
+++ b/ide/session.ml
@@ -0,0 +1,157 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Preferences
+
+let prefs = Preferences.current
+
+(** A session is a script buffer + proof + messages,
+    interacting with a coqtop, and a few other elements around *)
+
+type session = {
+  buffer : GText.buffer;
+  script : Wg_ScriptView.script_view;
+  proof : Wg_ProofView.proof_view;
+  messages : Wg_MessageView.message_view;
+  fileops : FileOps.ops;
+  coqops : CoqOps.ops;
+  coqtop : Coq.coqtop;
+  command : Wg_Command.command_window;
+  finder : Wg_Find.finder;
+  tab_label : GMisc.label;
+}
+
+type print_items =
+    (Coq.PrintOpt.t list * string * string * string * bool) list
+
+let create file coqtop_args print_items =
+  let basename = match file with
+    |None -> "*scratch*"
+    |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f)
+  in
+  let coqtop = Coq.spawn_coqtop coqtop_args in
+  let reset () = Coq.reset_coqtop coqtop
+  in
+  let buffer = GSourceView2.source_buffer
+    ~tag_table:Tags.Script.table
+    ~highlight_matching_brackets:true
+    ?language:(lang_manager#language prefs.source_language)
+    ?style_scheme:(style_manager#style_scheme prefs.source_style)
+    ()
+  in
+  let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
+  let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
+  let _ = buffer#place_cursor ~where:buffer#start_iter in
+  let _ = buffer#add_selection_clipboard Ideutils.cb
+  in
+  let script = Wg_ScriptView.script_view coqtop ~source_buffer:buffer
+    ~show_line_numbers:true ~wrap_mode:`NONE ()
+  in
+  let _ = script#misc#set_name "ScriptWindow"
+  in
+  let proof = Wg_ProofView.proof_view () in
+  let _ = proof#misc#set_can_focus true in
+  let _ =
+    GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION]
+  in
+  let messages = Wg_MessageView.message_view () in
+  let _ = messages#misc#set_can_focus true
+  in
+  let command = new Wg_Command.command_window coqtop in
+  let finder = new Wg_Find.finder (script :> GText.view) in
+  let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
+  let cops = new CoqOps.coqops script proof messages (fun () -> fops#filename)
+  in
+  let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in
+  let _ = fops#update_stats in
+  let _ = Coq.init_coqtop coqtop
+    (fun h k ->
+      cops#include_file_dir_in_path h
+        (fun () ->
+          let fold accu (opts, _, _, _, dflt) =
+            List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts
+          in
+          let options = List.fold_left fold [] print_items in
+          Coq.PrintOpt.set options h k))
+  in
+  {
+    buffer = (buffer :> GText.buffer);
+    script=script;
+    proof=proof;
+    messages=messages;
+    fileops=fops;
+    coqops=cops;
+    coqtop=coqtop;
+    command=command;
+    finder=finder;
+    tab_label= GMisc.label ~text:basename ();
+  }
+
+let kill (sn:session) =
+  (* To close the detached views of this script, we call manually
+     [destroy] on it, triggering some callbacks in [detach_view].
+     In a more modern lablgtk, rather use the page-removed signal ? *)
+  sn.script#destroy ();
+  Coq.close_coqtop sn.coqtop
+
+let build_layout (sn:session) =
+  let session_paned = GPack.paned `VERTICAL () in
+  let session_box =
+    GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) ()
+  in
+  let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
+    ~packing:(session_box#pack ~expand:true) () in
+  let script_frame = GBin.frame ~shadow_type:`IN
+    ~packing:eval_paned#add1 () in
+  let script_scroll = GBin.scrolled_window
+    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
+  let state_paned = GPack.paned `VERTICAL
+    ~packing:eval_paned#add2 () in
+  let proof_frame = GBin.frame ~shadow_type:`IN
+    ~packing:state_paned#add1 () in
+  let proof_scroll = GBin.scrolled_window
+    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in
+  let message_frame = GBin.frame ~shadow_type:`IN
+    ~packing:state_paned#add2 () in
+  let message_scroll = GBin.scrolled_window
+    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in
+  let session_tab = GPack.hbox ~homogeneous:false () in
+  let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
+    ~packing:session_tab#pack () in
+  let _ =
+    sn.buffer#connect#modified_changed
+      ~callback:(fun () -> if sn.buffer#modified
+        then img#set_stock `SAVE
+        else img#set_stock `YES) in
+  let _ =
+    eval_paned#misc#connect#size_allocate
+      ~callback:
+      (let old_paned_width = ref 2 in
+       let old_paned_height = ref 2 in
+       fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
+         if !old_paned_width <> paned_width ||
+            !old_paned_height <> paned_height
+         then begin
+           eval_paned#set_position
+             (eval_paned#position * paned_width / !old_paned_width);
+           state_paned#set_position
+             (state_paned#position * paned_height / !old_paned_height);
+           old_paned_width := paned_width;
+           old_paned_height := paned_height;
+	 end)
+  in
+  session_box#pack sn.finder#coerce;
+  session_paned#pack2 ~shrink:false ~resize:false (sn.command#frame#coerce);
+  script_scroll#add sn.script#coerce;
+  proof_scroll#add sn.proof#coerce;
+  message_scroll#add sn.messages#coerce;
+  session_tab#pack sn.tab_label#coerce;
+  img#set_stock `YES;
+  eval_paned#set_position 1;
+  state_paned#set_position 1;
+  (Some session_tab#coerce,None,session_paned#coerce)
diff --git a/ide/session.mli b/ide/session.mli
new file mode 100644
index 000000000..75b03d860
--- /dev/null
+++ b/ide/session.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** A session is a script buffer + proof + messages,
+    interacting with a coqtop, and a few other elements around *)
+
+type session = {
+  buffer : GText.buffer;
+  script : Wg_ScriptView.script_view;
+  proof : Wg_ProofView.proof_view;
+  messages : Wg_MessageView.message_view;
+  fileops : FileOps.ops;
+  coqops : CoqOps.ops;
+  coqtop : Coq.coqtop;
+  command : Wg_Command.command_window;
+  finder : Wg_Find.finder;
+  tab_label : GMisc.label;
+}
+
+type print_items =
+    (Coq.PrintOpt.t list * string * string * string * bool) list
+
+(** [create filename coqtop_args] *)
+val create : string option -> string list -> print_items -> session
+
+val kill : session -> unit
+
+val build_layout : session ->
+  GObj.widget option * GObj.widget option * GObj.widget
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index bd6d517dc..ad3b8ecc0 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -9,9 +9,13 @@
 class type message_view =
   object
     inherit GObj.widget
-    method clear : unit -> unit
+    method clear : unit
+    method add : string -> unit
+    method set : string -> unit
     method push : Interface.message_level -> string -> unit
+      (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
+      (** for more advanced text edition *)
   end
 
 let message_view () : message_view =
@@ -22,10 +26,10 @@ let message_view () : message_view =
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   let () = view#set_left_margin 2 in
-  object
+  object (self)
     inherit GObj.widget view#as_widget
 
-    method clear () =
+    method clear =
       buffer#set_text ""
 
     method push level msg =
@@ -36,6 +40,10 @@ let message_view () : message_view =
       buffer#insert ~tags msg;
       buffer#insert ~tags "\n"
 
+    method add msg = self#push Interface.Notice msg
+
+    method set msg = self#clear; self#add msg
+
     method buffer = buffer
 
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index f27f99afa..215521cda 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -9,9 +9,13 @@
 class type message_view =
   object
     inherit GObj.widget
-    method clear : unit -> unit
+    method clear : unit
+    method add : string -> unit
+    method set : string -> unit
     method push : Interface.message_level -> string -> unit
+      (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
+      (** for more advanced text edition *)
   end
 
 val message_view : unit -> message_view
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 0ab946d65..90eb78ca5 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -111,6 +111,10 @@ object (self)
       Minilib.log "==========Redo Stack End=========="
     end
 
+  method recenter_insert =
+    self#scroll_to_mark
+      ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
+
   method clear_undo () =
     history <- [];
     redo <- []
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index efe33f54d..4dabe6f33 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -24,6 +24,7 @@ object
   method set_show_right_margin : bool -> unit
   method comment : unit -> unit
   method uncomment : unit -> unit
+  method recenter_insert : unit
 end
 
 val script_view : Coq.coqtop ->