From e0f8d741b933361fc33a4ccd683b0137c869c468 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 10 Oct 2013 11:22:52 +0000 Subject: 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 --- ide/document.ml | 211 ++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 135 insertions(+), 76 deletions(-) (limited to 'ide/document.ml') 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 -- cgit v1.2.3