CoqIDE: move cmd_stack to a separate module: Document

The idea is to move the logic related to document handling
to a separate module that can be tested by fake_ide too.
CoqOps should "only" interface Document with the GtkTextBuffer.

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

1 files changed, 135 insertions, 76 deletions

diff --git a/ide/document.ml b/ide/document.ml
index 96ec05624..9b048320a 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -6,94 +6,153 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-exception Empty = Stack.Empty
+exception Empty
 
-type 'a t = {
-  mutable stack : 'a list;
-  mutable context : ('a list * 'a list) option
-}
+let invalid_arg s = raise (Invalid_argument ("Document."^s))
+
+type 'a sentence = { mutable state_id : Stateid.t option; data : 'a }
 
+type id = Stateid.t
+type 'a document = {
+  mutable stack : 'a sentence list;
+  mutable context : ('a sentence list * 'a sentence list) option
+}
+  
 let create () = { stack = []; context = None }
 
-let push x s = s.stack <- x :: s.stack
-
-let pop = function
-  | { stack = [] } -> raise Stack.Empty
-  | { stack = x::xs } as s -> s.stack <- xs; x
+(* Invariant, only the tip is a allowed to have state_id = None *)
+let invariant l = l = [] || (List.hd l).state_id <> None
 
 let tip = function
-  | { stack = [] } -> raise Stack.Empty
-  | { stack = x::_ } -> x
+  | { stack = [] } -> raise Empty
+  | { stack = { state_id = Some id }::_ } -> id
+  | { stack = { state_id = None }::_ } -> invalid_arg "tip"
+  
+let tip_data = function
+  | { stack = [] } -> raise Empty
+  | { stack = { data }::_ } -> data
+
+let push d x =
+  assert(invariant d.stack);
+  d.stack <- { data = x; state_id = None } :: d.stack
 
-let to_list = function
-  | { context = None; stack = s } -> s
-  | { context = Some (a,b); stack = s } -> a @ s @ b
+let pop = function
+  | { stack = [] } -> raise Empty
+  | { stack = { data }::xs } as s -> s.stack <- xs; data
+  
+let focus d ~cond_top:c_start ~cond_bot:c_stop =
+  assert(invariant d.stack);
+  if d.context <> None then invalid_arg "focus";
+  let rec aux (a,s,b) grab = function
+    | [] -> invalid_arg "focus"
+    | { state_id = Some id; data } as x :: xs when not grab ->
+        if c_start id data then aux (a,s,b) true (x::xs)
+        else aux (x::a,s,b) grab xs
+    | { state_id = Some id; data } as x :: xs ->
+        if c_stop id data then List.rev a, List.rev (x::s), xs
+        else aux (a,x::s,b) grab xs 
+    | _ -> assert false in
+  let a, s, b = aux ([],[],[]) false d.stack in
+  d.stack <- s;
+  d.context <- Some (a, b)
+  
+let unfocus = function
+  | { context = None } -> invalid_arg "unfocus"
+  | { context = Some (a,b); stack } as d ->
+       assert(invariant stack);
+       d.context <- None;
+       d.stack <- a @ stack @ b
+  
+let focused { context } = context <> None
 
 let to_lists = function
   | { context = None; stack = s } -> [],s,[]
   | { context = Some (a,b); stack = s } -> a,s,b
 
-let find f s =
-  let a, s, b = to_lists s in
-  try List.find (fun x -> f x false) a with Not_found ->
-  try List.find (fun x -> f x true)  s with Not_found ->
-      List.find (fun x -> f x false) b
-
-let find_map f s =
-  let rec aux b = function
-  | [] -> raise Not_found
-  | x :: xs -> match f x b with None -> aux b xs | Some i -> i
-  in
-  let a, s, b = to_lists s in
-  try aux false a with Not_found -> 
-  try aux true s  with Not_found -> 
-      aux false b
-
-type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c
-
-let fold_until f accu s =
-  let rec aux accu = function
-    | [] -> raise Not_found
-    | x :: xs -> match f accu x with Stop x -> x | Next i -> aux i xs in
-  aux accu s.stack
-
+let flat f b = fun x -> f b x.state_id x.data
+
+let find d f =
+  let a, s, b = to_lists d in
+  (
+  try List.find (flat f false) a with Not_found ->
+  try List.find (flat f true)  s with Not_found ->
+      List.find (flat f false) b
+  ).data
+  
+let find_map d f =
+  let a, s, b = to_lists d in
+  try CList.find_map (flat f false) a with Not_found -> 
+  try CList.find_map (flat f true)  s with Not_found -> 
+      CList.find_map (flat f false) b
+  
 let is_empty = function
   | { stack = []; context = None } -> true
   | _ -> false
-
-let iter f = function
-  | { stack = s; context = None } -> List.iter (fun x -> f x true) s
-  | { stack = s; context = Some(a,b) } ->
-        List.iter (fun x -> f x false) a;
-        List.iter (fun x -> f x true)  s;
-        List.iter (fun x -> f x false) b
-
-let clear s = s.stack <- []; s.context <- None
-
-let length = function
-  | { stack = s; context = None } -> List.length s
-  | { stack = s; context = Some(a,b) } ->
-        List.length a + List.length s + List.length b
-
-let focus s ~cond_top:c_start ~cond_bot:c_stop =
-  if s.context <> None then raise (Invalid_argument "CStack.focus");
-  let rec aux (a,s,b) grab = function
-    | [] -> raise (Invalid_argument "CStack.focus")
-    | x::xs when not grab ->
-        if c_start x then aux (a,s,b) true (x::xs)
-        else aux (x::a,s,b) grab xs
-    | x::xs ->
-        if c_stop x then a, x::s, xs
-        else aux (a,x::s,b) grab xs in
-  let a, stack, b = aux ([],[],[]) false s.stack in
-  s.stack <- List.rev stack;
-  s.context <- Some (List.rev a, b)
-
-let unfocus = function
-  | { context = None } -> raise (Invalid_argument "CStack.unfocus")
-  | { context = Some (a,b); stack } as s ->
-       s.context <- None;
-       s.stack <- a @ stack @ b
-
-let focused { context } = context <> None
-
+  
+let context d =
+  let top, _, bot = to_lists d in
+  let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
+  List.map (flat pair true) top, List.map (flat pair true) bot
+
+let iter d f =
+  let a, s, b = to_lists d in
+  List.iter (flat f false) a;
+  List.iter (flat f true)  s;
+  List.iter (flat f false) b
+  
+let stateid_opt_equal = Option.equal Stateid.equal
+
+let is_in_focus d id =
+  let _, focused, _ = to_lists d in
+  List.exists (fun { state_id } -> stateid_opt_equal state_id (Some id)) focused
+
+let clear d = d.stack <- []; d.context <- None
+  
+let print d f =
+  let top, mid, bot = to_lists d in
+  let open Pp in
+  v 0
+    (List.fold_right (fun i acc -> acc ++ cut() ++ flat f false i) top
+    (List.fold_right (fun i acc -> acc ++ cut() ++ flat f true i)  mid
+    (List.fold_right (fun i acc -> acc ++ cut() ++ flat f false i) bot (mt()))))
+
+let assign_tip_id d id =
+  match d with
+  | { stack = { state_id = None } as top :: _ } -> top.state_id <- Some id
+  | _ -> invalid_arg "assign_tip_id"
+
+let cut_at d id =
+  let aux (n, zone) { state_id; data } =
+    if stateid_opt_equal state_id (Some id) then CSig.Stop (n, List.rev zone)
+    else CSig.Cont (n + 1, data :: zone) in
+  let n, zone = CList.fold_left_until aux (0, []) d.stack in
+  for i = 1 to n do ignore(pop d) done;
+  zone
+
+let find_id d f =
+  let top, focus, bot = to_lists d in
+  let pred = function
+    | { state_id = Some id; data } when f id data -> Some id
+    | _ -> None in
+  try CList.find_map pred top, true with Not_found ->
+  try CList.find_map pred focus, focused d with Not_found ->
+      CList.find_map pred bot, true
+
+let before_tip d =
+  let _, focused, rest = to_lists d in
+  match focused with
+  | _:: { state_id = Some id } :: _ -> id, false
+  | _:: { state_id = None } :: _ -> assert false
+  | [] -> raise Not_found
+  | [_] ->
+      match rest with
+      | { state_id = Some id } :: _ -> id, true
+      | { state_id = None } :: _ -> assert false
+      | [] -> raise Not_found
+
+let fold_all d a f =
+  let top, focused, bot = to_lists d in
+  let a = List.fold_left (fun a -> flat (f a) false) a top in
+  let a = List.fold_left (fun a -> flat (f a) true)  a focused in
+  let a = List.fold_left (fun a -> flat (f a) false) a bot in
+  a