From 464abb8a8c5c6c9dcfad5ce143925a2889485496 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Mon, 7 Oct 2013 16:17:45 +0000 Subject: CoqIDE: cStack -> Document git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqOps.ml | 60 +++++++++++++++++----------------- ide/document.ml | 99 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ide/document.mli | 82 ++++++++++++++++++++++++++++++++++++++++++++++ ide/ide.mllib | 1 + 4 files changed, 212 insertions(+), 30 deletions(-) create mode 100644 ide/document.ml create mode 100644 ide/document.mli diff --git a/ide/coqOps.ml b/ide/coqOps.ml index be0cf9512..4a7711491 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -149,7 +149,7 @@ object(self) val proof = _pv val messages = _mv - val cmd_stack = Stack.create () + val cmd_stack = Document.create () val mutable initial_state = Stateid.initial @@ -175,11 +175,11 @@ object(self) let marks = iter#marks in if marks = [] then aux iter#backward_char else - let mem_marks s = + let mem_marks s _ = List.exists (fun m -> Gobject.get_oid m = Gobject.get_oid (buffer#get_mark s.start)) marks in - try Stack.find mem_marks cmd_stack + try Document.find mem_marks cmd_stack with Not_found -> aux iter#backward_char in aux iter in let ss = @@ -198,25 +198,25 @@ object(self) method private print_stack = Minilib.log "cmd_stack:"; - let top, mid, bot = Stack.to_lists cmd_stack in + let top, mid, bot = Document.to_lists cmd_stack in Minilib.log "--start--"; List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) top; - if Stack.focused cmd_stack then Minilib.log "----"; + if Document.focused cmd_stack then Minilib.log "----"; List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) mid; - if Stack.focused cmd_stack then Minilib.log "----"; + if Document.focused cmd_stack then Minilib.log "----"; List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) bot; Minilib.log "--stop--" method private enter_focus start stop to_id tip = - if Stack.focused cmd_stack then begin + if Document.focused cmd_stack then begin self#exit_focus tip end; let at id s = s.state_id = Some id in self#print_stack; Minilib.log("Focusing "^Stateid.to_string start^" "^Stateid.to_string stop); - Stack.focus cmd_stack ~cond_top:(at start) ~cond_bot:(at stop); + Document.focus cmd_stack ~cond_top:(at start) ~cond_bot:(at stop); self#print_stack; - let qed_s = Stack.top cmd_stack in + let qed_s = Document.tip cmd_stack in buffer#apply_tag Tags.Script.read_only ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char (fun c -> not(Glib.Unichar.isspace c))) @@ -227,15 +227,15 @@ object(self) method private exit_focus newtip = self#print_stack; Minilib.log "Unfocusing"; - Stack.unfocus cmd_stack; + Document.unfocus cmd_stack; self#print_stack; - if (Some newtip <> (Stack.top cmd_stack).state_id) then begin + if (Some newtip <> (Document.tip cmd_stack).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 (Stack.top cmd_stack).stop in + let where = buffer#get_iter_at_mark (Document.tip cmd_stack).stop in buffer#move_mark ~where (`NAME "start_of_input"); buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input") @@ -327,12 +327,12 @@ object(self) let msg = Queue.pop feedbacks in let id = msg.id in let sentence = - let finder s = + let finder s _ = match s.state_id, id with | Some id', State id when id = id' -> Some s | _, Edit id when id = s.edit_id -> Some s | _ -> None in - try Some (Stack.find_map finder cmd_stack) + try Some (Document.find_map finder cmd_stack) with Not_found -> None in let log s sentence = Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string @@ -367,9 +367,9 @@ object(self) | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" - else if Stack.is_empty cmd_stack then () + else if Document.is_empty cmd_stack then () else - match id, (Stack.top cmd_stack).state_id with + match id, (Document.tip cmd_stack).state_id with | Edit _, _ -> () | State id1, Some id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks (* Put back into the queue *) @@ -474,7 +474,7 @@ object(self) queue) in let tip = - try Stack.fold_until (fun () -> function + try Document.fold_until (fun () -> function | { state_id = Some id } -> Stop id | _ -> Next ()) () cmd_stack with Not_found -> initial_state in @@ -496,7 +496,7 @@ object(self) | `Sentence sentence, _ :: _ -> assert false | `Sentence sentence, [] -> add_flag sentence `PROCESSING; - Stack.push sentence cmd_stack; + Document.push sentence cmd_stack; if has_flag sentence `COMMENT then let () = remove_flag sentence `PROCESSING in let () = self#commit_queue_transaction sentence in @@ -514,14 +514,14 @@ object(self) loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> assign_state_id sentence id; - let topstack, _, _ = Stack.to_lists cmd_stack in + let topstack, _, _ = Document.to_lists cmd_stack 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 = Stack.pop cmd_stack in + let sentence = Document.pop cmd_stack in self#process_interp_error queue sentence loc msg id in Coq.bind query next @@ -542,7 +542,7 @@ object(self) method get_n_errors = List.fold_left (fun n s -> if has_flag s `ERROR then n+1 else n) - 0 (Stack.to_list cmd_stack) + 0 (Document.to_list cmd_stack) method get_errors = let extract_error s = @@ -552,7 +552,7 @@ object(self) CList.map_filter (fun s -> if has_flag s `ERROR then Some (extract_error s) else None) - (Stack.to_list cmd_stack) + (Document.to_list cmd_stack) method process_next_phrase = let until len start stop = 1 <= len in @@ -577,15 +577,15 @@ object(self) match found, state_id with | true, Some id -> Stop (n, id, Some sentence, zone) | _ -> Next (n + 1, found, sentence :: zone) in - try Stack.fold_until finder (0, false, []) cmd_stack + try Document.fold_until finder (0, false, []) cmd_stack with Not_found -> Minilib.log "ALL"; - Stack.length cmd_stack, initial_state, - None, List.rev (Stack.to_list cmd_stack) + Document.length cmd_stack, initial_state, + None, List.rev (Document.to_list cmd_stack) 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(Stack.pop cmd_stack) done; + for i = 1 to n do ignore(Document.pop cmd_stack) done; 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 @@ -688,7 +688,7 @@ object(self) ~start:(`MARK (buffer#create_mark start)) ~stop:(`MARK (buffer#create_mark stop)) [] in - Stack.push sentence cmd_stack; + Document.push sentence cmd_stack; messages#clear; self#show_goals in @@ -722,9 +722,9 @@ object(self) let action () = if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."; (* clear the stack *) - if Stack.focused cmd_stack then Stack.unfocus cmd_stack; - while not (Stack.is_empty cmd_stack) do - let phrase = Stack.pop cmd_stack in + if Document.focused cmd_stack then Document.unfocus cmd_stack; + while not (Document.is_empty cmd_stack) do + let phrase = Document.pop cmd_stack in buffer#delete_mark phrase.start; buffer#delete_mark phrase.stop done; diff --git a/ide/document.ml b/ide/document.ml new file mode 100644 index 000000000..96ec05624 --- /dev/null +++ b/ide/document.ml @@ -0,0 +1,99 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raise Stack.Empty + | { stack = x::xs } as s -> s.stack <- xs; x + +let tip = function + | { stack = [] } -> raise Stack.Empty + | { stack = x::_ } -> x + +let to_list = function + | { context = None; stack = s } -> s + | { context = Some (a,b); stack = s } -> a @ s @ b + +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 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 + diff --git a/ide/document.mli b/ide/document.mli new file mode 100644 index 000000000..c610f275c --- /dev/null +++ b/ide/document.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a t +(** Create an empty stack. *) + +val push : 'a -> 'a t -> unit +(** Add an element to a stack. *) + +val find : ('a -> bool -> bool) -> 'a t -> 'a +(** Find the first element satisfying the predicate. + The boolean tells If the element is inside the focused zone. + @raise Not_found it there is none. *) + +val is_empty : 'a t -> bool +(** Whether a stack is empty. *) + +val iter : ('a -> bool -> unit) -> 'a t -> unit +(** Iterate a function over elements, from the last added one. + The boolean tells If the element is inside the focused zone. *) + +val clear : 'a t -> unit +(** Empty a stack. *) + +val length : 'a t -> int +(** Length of a stack. *) + +val pop : 'a t -> 'a +(** Remove and returns the first element of the stack. + @raise Empty if empty. *) + +val tip : 'a t -> 'a +(** Remove the first element of the stack without modifying it. + @raise Empty if empty. *) + +val to_list : 'a t -> 'a list +(** Convert to a list. *) + +val find_map : ('a -> bool -> 'b option) -> 'a t -> 'b +(** Find the first element that returns [Some _]. + The boolean tells If the element is inside the focused zone. + @raise Not_found it there is none. *) + +type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c + +(** [seek f acc s] acts like [List.fold_left f acc s] while [f] returns + [Next acc']; it stops returning [b] as soon as [f] returns [Stop b]. + The stack is traversed from the top and is not altered. + @raise Not_found it there is none. *) +val fold_until : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b + +(** After [focus s c1 c2] the top of [s] is the topmost element [x] such that + [c1 x] is [true] and the bottom is the first element [y] following [x] + such that [c2 y] is [true]. After a focus push/pop/top/fold_until + only use the focused part. + @raise Invalid_argument "CStack.focus" if there is no such [x] and [y] *) +val focus : 'a t -> cond_top:('a -> bool) -> cond_bot:('a -> bool) -> unit + +(** Undoes a [focus]. + @raise Invalid_argument "CStack.unfocus" if the stack is not focused *) +val unfocus : 'a t -> unit + +(** Is the stack focused *) +val focused : 'a t -> bool + +(** Returns [top, s, bot] where [top @ s @ bot] is the full stack, and [s] + the focused part *) +val to_lists : 'a t -> 'a list * 'a list * 'a list + diff --git a/ide/ide.mllib b/ide/ide.mllib index ce4fcca0d..1c07f6c0e 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -27,6 +27,7 @@ Wg_ScriptView Coq_commands Wg_Command FileOps +Document CoqOps Session Coqide_ui -- cgit v1.2.3