CoqIDE: ported to Document

The code is simpler, but there is still room for improvement.
In particular find_id (implemented in both coqOps and fake_id)
should be part of Document.

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

1 files changed, 109 insertions, 154 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1246d3159..e59e7a85c 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -11,13 +11,12 @@ open Coq
 open Ideutils
 open Interface
 
-type flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR of string ]
-type mem_flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ]
+type flag = [ `UNSAFE | `PROCESSING | `ERROR of string ]
+type mem_flag = [ `UNSAFE | `PROCESSING | `ERROR ]
 let mem_flag_of_flag : flag -> mem_flag = function
   | `ERROR _ -> `ERROR
-  | (`COMMENT | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
+  | (`UNSAFE | `PROCESSING) as mem_flag -> mem_flag
 let str_of_flag = function
-  | `COMMENT -> "C"
   | `UNSAFE -> "U"
   | `PROCESSING -> "P"
   | `ERROR _ -> "E"
@@ -179,8 +178,8 @@ object(self)
             with Not_found -> aux iter#backward_char in
         aux iter in
       let ss =
-        find_all_tooltips s.Doc.data
-          (iter#offset - (buffer#get_iter_at_mark s.Doc.data.start)#offset) in
+        find_all_tooltips s
+          (iter#offset - (buffer#get_iter_at_mark s.start)#offset) in
       let msg = String.concat "\n" (CList.uniquize (List.map Lazy.force ss)) in
       GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON;
       script#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>")
@@ -196,11 +195,8 @@ object(self)
     Minilib.log "document:";
     Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
 
-  method private enter_focus start stop to_id tip =
-    if Doc.focused document then begin
-      self#exit_focus tip
-    end;
-    let at id s = s.Doc.state_id = Some id in
+  method private enter_focus start stop =
+    let at id id' _ = Stateid.equal id' id in
     self#print_stack;
     Minilib.log("Focusing "^Stateid.to_string start^" "^Stateid.to_string stop);
     Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
@@ -213,19 +209,20 @@ object(self)
     buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
       (`NAME "stop_of_input")
 
-  method private exit_focus newtip =
-    self#print_stack;
+  method private exit_focus =
     Minilib.log "Unfocusing";
+    begin try
+      let { start; stop } = Doc.tip_data document in
+      buffer#remove_tag Tags.Script.read_only
+        ~start:(buffer#get_iter_at_mark start)
+        ~stop:(buffer#get_iter_at_mark stop)
+    with Doc.Empty -> () end;
     Doc.unfocus document;
     self#print_stack;
-    if (Some newtip <> (Doc.tip document).Doc.state_id) then begin
-      Minilib.log ("Cutting tip to " ^ Stateid.to_string newtip);
-      let until id _ _ = id = Some newtip in
-      let n, _, _, seg = self#segment_to_be_cleared until in
-      self#cleanup n seg
-    end;
-    let where = buffer#get_iter_at_mark (Doc.tip_data document).stop in
-    buffer#move_mark ~where (`NAME "start_of_input");
+    begin try
+      let where = buffer#get_iter_at_mark (Doc.tip_data document).stop in
+      buffer#move_mark ~where (`NAME "start_of_input");
+    with Doc.Empty -> () end;
     buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input")
 
   method private get_start_of_input =
@@ -359,10 +356,12 @@ object(self)
           if sentence <> None then Minilib.log "Unsupported feedback message"
           else if Doc.is_empty document then ()
           else
-            match id, (Doc.tip document).Doc.state_id with
-            | Edit _, _ -> ()
-            | State id1, Some id2 when Stateid.newer_than id2 id1 -> ()
-            | _ -> Queue.add msg feedbacks (* Put back into the queue *)
+            try
+              match id, Doc.tip document with
+              | Edit _, _ -> ()
+              | State id1, id2 when Stateid.newer_than id2 id1 -> ()
+              | _ -> Queue.add msg feedbacks
+            with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks 
       end;
         eat_feedback (n-1)
     in
@@ -409,31 +408,27 @@ object(self)
       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 iter =
+    let rec loop n iter =
       match Sentence.find buffer iter with
       | None -> ()
       | Some (start, stop) ->
-        if until start stop then begin
+        if until n start stop then begin
           ()
         end else if start#has_tag Tags.Script.processed then begin
           Queue.push (`Skip (start, stop)) queue;
-          loop stop
+          loop n stop
         end else begin
           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 sentence =
             mk_sentence
               ~start:(`MARK (buffer#create_mark start))
               ~stop:(`MARK (buffer#create_mark stop))
-              (if is_comment then [`COMMENT] else []) in
+              [] in
           Queue.push (`Sentence sentence) queue;
-          if not stop#is_end then loop stop
+          if not stop#is_end then loop (succ n) stop
         end
     in
-    loop self#get_start_of_input
+    loop 0 self#get_start_of_input
 
   method private discard_command_queue queue =
     while not (Queue.is_empty queue) do
@@ -449,8 +444,8 @@ object(self)
 
   (** Compute the phrases until [until] returns [true]. *)
   method private process_until until verbose =
-    let push_msg lvl msg = if verbose then messages#push lvl msg in
-    let action = Coq.lift (fun () ->
+    let logger lvl msg = if verbose then messages#push lvl msg in
+    let fill_queue = Coq.lift (fun () ->
       let queue = Queue.create () in
       (* Lock everything and fill the waiting queue *)
       push_info "Coq is computing";
@@ -461,63 +456,53 @@ object(self)
         may contain iterators, it shouldn't be used anymore *)
       script#set_editable true;
       Minilib.log "Begin command processing";
-      queue)
-    in
-    let tip =
-      try Doc.fold_until document () (fun () -> function
-          | Some id -> fun _ -> Stop id
-          | _ -> fun _ -> Next ())
-      with Not_found -> initial_state in
-    Coq.bind action (fun queue ->
-    let rec loop tip topstack =
-      if Queue.is_empty queue then
-        let () = pop_info () in
-        let () = script#recenter_insert in
-        match topstack with
-        | [] -> self#show_goals
-        | s :: _ ->
-           self#backtrack_to_iter (buffer#get_iter_at_mark s.Doc.data.start)
-      else
+      queue) in
+    let conclude topstack =
+      pop_info ();
+      script#recenter_insert;
+      match topstack with
+      | [] -> self#show_goals
+      | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
+    let process_queue queue =
+      let rec loop tip topstack =
+        if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] -> assert false
-        | `Skip(start,stop), s :: topstack ->
-            assert(start#equal (buffer#get_iter_at_mark s.Doc.data.start));
-            assert(stop#equal (buffer#get_iter_at_mark s.Doc.data.stop));
+        | `Skip(start,stop), (_,s) :: topstack ->
+            assert(start#equal (buffer#get_iter_at_mark s.start));
+            assert(stop#equal (buffer#get_iter_at_mark s.stop));
             loop tip topstack
         | `Sentence sentence, _ :: _ -> assert false
-        | `Sentence sentence, [] ->
-        add_flag sentence `PROCESSING;
-        Doc.push document sentence;
-        if has_flag sentence `COMMENT then
-          let () = remove_flag sentence `PROCESSING in
-          let () = self#commit_queue_transaction sentence in
-          loop tip topstack
-        else
-          (* If the line is not a comment, we interpret it. *)
-          let _, _, phrase = self#get_sentence sentence in
-          let query =
-            Coq.add ~logger:push_msg ((phrase,sentence.edit_id),(tip,verbose))in
-          let next = function
-          | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
-              Doc.assign_tip_id document id;
-              push_msg Notice msg;
-              self#commit_queue_transaction sentence;
-              loop id []
-          | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
-              Doc.assign_tip_id document id;
-              let topstack, _, _ = Doc.to_lists document in
-              self#exit_focus tip;
-              push_msg Notice msg;
-              self#mark_as_needed sentence;
-              if Queue.is_empty queue then loop tip []
-              else loop tip (List.rev topstack)
-          | Fail (id, loc, msg) ->
-              let sentence = Doc.pop document in
-              self#process_interp_error queue sentence.Doc.data loc msg id
-          in
-          Coq.bind query next
-    in
-    loop tip [])
+        | `Sentence ({ edit_id } as sentence), [] ->
+            add_flag sentence `PROCESSING;
+            Doc.push document sentence;
+            let _, _, phrase = self#get_sentence sentence in
+            let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in
+            let handle_answer = function
+              | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
+                  Doc.assign_tip_id document id;
+                  logger Notice msg;
+                  self#commit_queue_transaction sentence;
+                  loop id []
+              | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
+                  Doc.assign_tip_id document id;
+                  let topstack, _ = Doc.context document in
+                  self#exit_focus;
+                  self#cleanup (Doc.cut_at document tip);
+                  logger Notice msg;
+                  self#mark_as_needed sentence;
+                  if Queue.is_empty queue then loop tip []
+                  else loop tip (List.rev topstack)
+              | Fail (id, loc, msg) ->
+                  let sentence = Doc.pop document in
+                  self#process_interp_error queue sentence loc msg id in
+            Coq.bind coq_query handle_answer
+      in
+      let tip =
+        try Doc.tip document
+        with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in
+      loop tip [] in
+    Coq.bind fill_queue process_queue
   
   method join_document =
    let next = function
@@ -530,30 +515,27 @@ object(self)
 
   method get_slaves_status = processed, to_process
 
-  method get_n_errors = 
-    List.fold_left
-      (fun n s -> if has_flag s.Doc.data `ERROR then n+1 else n)
-      0 (Doc.to_list document)
+  method get_n_errors =
+    Doc.fold_all document 0 (fun n _ _ s -> if has_flag s `ERROR then n+1 else n)
 
   method get_errors =
     let extract_error s =
       match List.find (function `ERROR _ -> true | _ -> false) s.flags with
       | `ERROR msg -> (buffer#get_iter_at_mark s.start)#line + 1, msg
       | _ -> assert false in
-    CList.map_filter (fun s ->
-      if has_flag s.Doc.data `ERROR then Some (extract_error s.Doc.data)
-      else None)
-      (Doc.to_list document)
+    List.rev
+      (Doc.fold_all document [] (fun acc _ _ s ->
+        if has_flag s `ERROR then extract_error s :: acc else acc))
 
   method process_next_phrase =
-    let until = let len = ref 0 in fun _ _ -> incr len; !len > 1 in
+    let until n _ _ = n >= 1 in
     let next () =
       buffer#place_cursor ~where:self#get_start_of_input; Coq.return ()
     in
     Coq.bind (self#process_until until true) next
 
   method private process_until_iter iter =
-    let until start stop =
+    let until _ start stop =
       if prefs.Preferences.stop_before then stop#compare iter > 0
       else start#compare iter >= 0
     in
@@ -564,38 +546,15 @@ object(self)
 
   (* finds the state_id and if it an unfocus is needed to reach it *)
   method private find_id until =
-    let focused = Doc.focused document in
-    try
-      Doc.find_map document (fun b ->
-        function
-        | Some id -> fun { start; stop } ->
-           if until (Some id) start stop then
-             Some (id, if focused then not b else false)
-           else
-             None
-        | None -> fun { start; stop } -> None)
-    with Not_found -> initial_state, focused 
-
-  method private segment_to_be_cleared until =
-    let finder (n, found, zone) state_id ({ start; stop } as sentence) =
-      let found = found || until state_id start stop in
-      match found, state_id with
-      | true, Some id -> Stop (n, id, Some sentence, zone)
-      | _ -> Next (n + 1, found, sentence :: zone) in
-    try Doc.fold_until document (0, false, []) finder
-    with Not_found ->
-            Minilib.log "XXX ALL XXX";
-      Doc.length document, initial_state,
-      None, List.rev (List.map (fun x -> x.Doc.data) (Doc.to_list document))
-
-  method private cleanup n seg =
-    Minilib.log("Clean "^string_of_int n^" "^string_of_int(List.length seg));
-    for i = 1 to n do ignore(Doc.pop document) done;
+    try Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
+    with Not_found -> initial_state, Doc.focused document 
+
+  method private cleanup seg =
     if seg <> [] then begin
-      let start = buffer#get_iter_at_mark (CList.hd seg).start in
-      let stop = buffer#get_iter_at_mark (CList.last seg).stop in
-      Minilib.log("Clean tags in range "^string_of_int start#offset^
-        " "^string_of_int stop#offset);
+      let start = buffer#get_iter_at_mark (CList.last seg).start in
+      let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
+      Minilib.log
+        (Printf.sprintf "Clean tags in range %d -> %d" start#offset stop#offset);
       buffer#remove_tag Tags.Script.processed ~start ~stop;
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
@@ -606,7 +565,7 @@ object(self)
     List.iter (fun { stop } -> buffer#delete_mark stop) seg
 
   (** Wrapper around the raw undo command *)
-  method private backtrack_until ?(move_insert=true) until =
+  method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
     let opening () =
       push_info "Coq is undoing" in
     let conclusion () =
@@ -622,32 +581,27 @@ object(self)
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
       self#show_goals in
     Coq.bind (Coq.lift opening) (fun () ->
-    let rec undo until =
-      let to_id, unfocus_needed = self#find_id until in
+    let rec undo to_id unfocus_needed =
       Coq.bind (Coq.edit_at to_id) (function
       | Good (CSig.Inl (* NewTip *) ()) ->
-          if unfocus_needed then self#exit_focus to_id
-          else begin
-            let n, to_id, sentence, seg =
-              self#segment_to_be_cleared (fun id _ _ -> id = Some to_id) in
-            self#cleanup n seg
-          end;
+          if unfocus_needed then self#exit_focus;
+          self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Good (CSig.Inr (* Focus  *) (stop_id,(start_id,tip))) ->
-          if unfocus_needed then self#exit_focus tip
-          else begin
-            self#enter_focus start_id stop_id to_id tip;
-            let n, to_id, sentence, seg =
-              self#segment_to_be_cleared (fun id _ _ -> id = Some to_id) in
-            self#cleanup n seg
-          end;
+          if unfocus_needed then self#exit_focus;
+          self#cleanup (Doc.cut_at document tip);
+          self#enter_focus start_id stop_id;
+          self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Error "Fixme LOC";
           messages#push Error msg;
-          undo (fun id _ _ -> id = Some safe_id))
+          undo safe_id (Doc.is_in_focus document safe_id))
     in
-      undo until)
+      undo to_id unfocus_needed)
+  
+  method private backtrack_until ?move_insert until =
+    self#backtrack_to_id ?move_insert (self#find_id until)
 
   method private backtrack_to_iter ?move_insert iter =
     let until _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in
@@ -665,10 +619,11 @@ object(self)
         script#scroll_mark_onscreen (`NAME "start_of_input")))
 
   method backtrack_last_phrase =
-    let id = (Doc.tip document).Doc.state_id in
-    let until sid _ _ = sid <> id in
     messages#clear;
-    self#backtrack_until until
+    try 
+      let tgt = Doc.before_tip document in
+      self#backtrack_to_id tgt
+    with Not_found -> Coq.return (Coq.reset_coqtop _ct)
 
   method go_to_insert =
     Coq.bind (Coq.return ()) (fun () ->
@@ -739,8 +694,8 @@ object(self)
       if Doc.focused document then Doc.unfocus document;
       while not (Doc.is_empty document) do
         let phrase = Doc.pop document in
-        buffer#delete_mark phrase.Doc.data.start;
-        buffer#delete_mark phrase.Doc.data.stop
+        buffer#delete_mark phrase.start;
+        buffer#delete_mark phrase.stop
       done;
       List.iter
         (buffer#remove_tag ~start:buffer#start_iter ~stop:buffer#end_iter)