aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-07 16:17:45 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-07 16:17:45 +0000
commit464abb8a8c5c6c9dcfad5ce143925a2889485496 (patch)
tree9752daed0e36dc0bc4170f9d65fa86525ef5d614 /ide/coqOps.ml
parent7daef0b418e87f39019eacf72a1230f7616c2a53 (diff)
CoqIDE: cStack -> Document
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml60
1 files changed, 30 insertions, 30 deletions
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;