From c2619b368b352f6f776360356a4f9112095efc06 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 10 Oct 2013 11:22:53 +0000 Subject: 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 --- ide/coqOps.ml | 263 ++++++++++++++++++++++++---------------------------------- 1 file changed, 109 insertions(+), 154 deletions(-) (limited to 'ide/coqOps.ml') 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 ("" ^ msg ^ "") @@ -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) -- cgit v1.2.3