diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 8 | ||||
| -rw-r--r-- | ide/coq.mli | 12 | ||||
| -rw-r--r-- | ide/coqOps.ml | 278 | ||||
| -rw-r--r-- | ide/sentence.ml | 9 | ||||
| -rw-r--r-- | ide/session.ml | 69 | ||||
| -rw-r--r-- | ide/tags.ml | 10 | ||||
| -rw-r--r-- | ide/tags.mli | 4 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 4 |
8 files changed, 280 insertions, 114 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index be35ebe1a..96a19f317 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -370,7 +370,7 @@ let handle_final_answer handle xml = | None -> raise AnswerWithoutRequest | Some (c, _) -> c in let () = handle.waiting_for <- None in - with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer xml c) } + with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) } type input_state = { mutable fragment : string; @@ -558,9 +558,9 @@ let eval_call ?(logger=default_logger) call handle k = Minilib.log "End eval_call"; Void -let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s = - eval_call ~logger (Serialize.interp (i,raw,verbose,s)) -let backto i = eval_call (Serialize.backto i) +let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x) +let edit_at i = eval_call (Serialize.edit_at i) +let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x) let inloadpath s = eval_call (Serialize.inloadpath s) let mkcases s = eval_call (Serialize.mkcases s) let status ?logger force = eval_call ?logger (Serialize.status force) diff --git a/ide/coq.mli b/ide/coq.mli index 330cc776f..4fe6a2188 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -122,13 +122,13 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit type 'a query = 'a Interface.value task (** A type abbreviation for coqtop specific answers *) -val interp : ?logger:Ideutils.logger -> - ?raw:bool -> - ?verbose:bool -> - Interface.edit_id -> string -> Interface.interp_rty query -val backto : Interface.backto_sty -> Interface.backto_rty query +val add : ?logger:Ideutils.logger -> + Interface.add_sty -> Interface.add_rty query +val edit_at : Interface.edit_at_sty -> Interface.edit_at_rty query +val query : ?logger:Ideutils.logger -> + Interface.query_sty -> Interface.query_rty query val status : ?logger:Ideutils.logger -> - Interface.status_sty -> Interface.status_rty query + Interface.status_sty -> Interface.status_rty query val goals : ?logger:Ideutils.logger -> Interface.goals_sty -> Interface.goals_rty query val evars : Interface.evars_sty -> Interface.evars_rty query diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 081cf62d4..1deb0a8ba 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -16,6 +16,11 @@ type mem_flag = [ `COMMENT | `UNSAFE | `PROCESSING | `ERROR ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR | (`COMMENT | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag +let str_of_flag = function + | `COMMENT -> "C" + | `UNSAFE -> "U" + | `PROCESSING -> "P" + | `ERROR _ -> "E" module SentenceId : sig @@ -38,6 +43,8 @@ module SentenceId : sig val same_sentence : sentence -> sentence -> bool val hidden_edit_id : unit -> int + val dbg_to_string : GText.buffer -> sentence -> string + end = struct type sentence = { @@ -67,9 +74,24 @@ end = struct let has_flag s mf = List.exists (fun f -> mem_flag_of_flag f = mf) s.flags let remove_flag s mf = - s.flags <- List.filter (fun f -> mem_flag_of_flag f = mf) s.flags + s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags let same_sentence s1 s2 = s1.edit_id = s2.edit_id && s1.state_id = s2.state_id + let dbg_to_string (b : GText.buffer) s = + let ellipsize s = + Str.global_replace (Str.regexp "^[\n ]*") "" + (if String.length s > 20 then String.sub s 0 17 ^ "..." + else s) in + Printf.sprintf "[%3d,%3s](%5d,%5d) %s [%s]" + s.edit_id + (Stateid.to_string (Option.default Stateid.dummy s.state_id)) + (b#get_iter_at_mark s.start)#offset + (b#get_iter_at_mark s.stop)#offset + (ellipsize + ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop))) + (String.concat "," (List.map str_of_flag s.flags)) + + end open SentenceId @@ -132,8 +154,54 @@ object(self) method destroy () = feedback_timer.Ideutils.kill () + method private print_stack = + Minilib.log "cmd_stack:"; + let top, mid, bot = Stack.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 "----"; + List.iter (fun s -> Minilib.log(dbg_to_string buffer s)) mid; + if Stack.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 + 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); + self#print_stack; + let qed_s = Stack.top 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))) + ~stop:(buffer#get_iter_at_mark qed_s.stop); + buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop) + (`NAME "stop_of_input") + + method private exit_focus newtip = + self#print_stack; + Minilib.log "Unfocusing"; + Stack.unfocus cmd_stack; + self#print_stack; + if (Some newtip <> (Stack.top 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 + buffer#move_mark ~where (`NAME "start_of_input"); + buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input") + method private get_start_of_input = buffer#get_iter_at_mark (`NAME "start_of_input") + + method private get_end_of_input = + buffer#get_iter_at_mark (`NAME "stop_of_input") method private get_insert = buffer#get_iter_at_mark `INSERT @@ -162,56 +230,23 @@ object(self) else messages#add s; in let query = - Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in + Coq.query ~logger:messages#push (phrase,Stateid.dummy) in let next = function - | Fail (_, _, err) -> display_error err; Coq.return () (* XXX*) - | Good (_, msg) -> + | Fail (_, _, err) -> display_error err; Coq.return () + | Good msg -> messages#add msg; Coq.return () in Coq.bind (Coq.seq action query) next - (** [fill_command_queue until q] fills a command queue until the [until] - 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 len iter = - match Sentence.find buffer iter with - | None -> raise Exit - | Some (start, stop) -> - if until len start stop then raise Exit; - 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 - Queue.push sentence queue; - if not stop#is_end then loop (succ len) stop - in - try loop 0 self#get_start_of_input with Exit -> () - - method private discard_command_queue queue = - while not (Queue.is_empty queue) do - let sentence = Queue.pop queue in - let start = buffer#get_iter_at_mark sentence.start in - let stop = buffer#get_iter_at_mark sentence.stop in - buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#delete_mark sentence.start; - buffer#delete_mark sentence.stop; - done - method private mark_as_needed sentence = + Minilib.log("Marking " ^ dbg_to_string buffer sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in let processed = Tags.Script.processed in let unjustified = Tags.Script.unjustified in let error_bg = Tags.Script.error_bg in - let all_tags = [ to_process; processed; unjustified ] in + let all_tags = [ error_bg; to_process; processed; unjustified ] in let tags = (if has_flag sentence `PROCESSING then to_process else if has_flag sentence `ERROR then error_bg else @@ -326,7 +361,7 @@ object(self) self#discard_command_queue queue; pop_info (); self#position_error_tag_at_iter start phrase loc; - buffer#place_cursor ~where:start; + buffer#place_cursor ~where:stop; messages#clear; messages#push Error msg; self#show_goals) @@ -337,6 +372,48 @@ object(self) let phrase = start#get_slice ~stop in start, stop, phrase + (** [fill_command_queue until q] fills a command queue until the [until] + 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 len iter = + match Sentence.find buffer iter with + | None -> () + | Some (start, stop) -> + if until len start stop then begin + () + end else if start#has_tag Tags.Script.processed then begin + Queue.push (`Skip (start, stop)) queue; + loop len 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 + Queue.push (`Sentence sentence) queue; + if not stop#is_end then loop (succ len) stop + end + in + loop 0 self#get_start_of_input + + method private discard_command_queue queue = + while not (Queue.is_empty queue) do + match Queue.pop queue with + | `Skip _ -> () + | `Sentence sentence -> + let start = buffer#get_iter_at_mark sentence.start in + let stop = buffer#get_iter_at_mark sentence.stop in + buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#delete_mark sentence.start; + buffer#delete_mark sentence.stop; + done + (** 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 @@ -353,41 +430,59 @@ object(self) Minilib.log "Begin command processing"; queue) in + let tip = + try Stack.fold_until (fun () -> function + | { state_id = Some id } -> Stop id + | _ -> Next ()) () cmd_stack + with Not_found -> initial_state in Coq.bind action (fun queue -> - let rec loop () = + let rec loop tip topstack = if Queue.is_empty queue then let () = pop_info () in let () = script#recenter_insert in - self#show_goals + match topstack with + | [] -> self#show_goals + | s :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) else - let sentence = Queue.pop queue in + 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.start)); + assert(stop#equal (buffer#get_iter_at_mark s.stop)); + loop tip topstack + | `Sentence sentence, _ :: _ -> assert false + | `Sentence sentence, [] -> add_flag sentence `PROCESSING; Stack.push sentence cmd_stack; if has_flag sentence `COMMENT then let () = remove_flag sentence `PROCESSING in let () = self#commit_queue_transaction sentence in - loop () + loop tip topstack else (* If the line is not a comment, we interpret it. *) let _, _, phrase = self#get_sentence sentence in - let commit_and_continue msg = - push_msg Notice msg; - self#commit_queue_transaction sentence; - loop () - in let query = - Coq.interp ~logger:push_msg ~verbose sentence.edit_id phrase in + Coq.add ~logger:push_msg ((phrase,sentence.edit_id),(tip,verbose))in let next = function - | Good (id, msg) -> + | Good (id, (Util.Inl (* NewTip *) (), msg)) -> + assign_state_id sentence id; + push_msg Notice msg; + self#commit_queue_transaction sentence; + loop id [] + | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> assign_state_id sentence id; - commit_and_continue msg + let topstack, _, _ = Stack.to_lists cmd_stack in + self#exit_focus tip; + push_msg Notice msg; + self#mark_as_needed sentence; + loop tip (List.rev topstack) | Fail (id, loc, msg) -> let sentence = Stack.pop cmd_stack in self#process_interp_error queue sentence loc msg id in Coq.bind query next in - loop ()) + loop tip []) method join_document = let next = function @@ -430,7 +525,7 @@ object(self) self#process_until until false method process_until_end_or_error = - self#process_until_iter buffer#end_iter + self#process_until_iter self#get_end_of_input method private segment_to_be_cleared until = let finder (n, found, zone) ({ start; stop; state_id } as sentence) = @@ -438,11 +533,29 @@ 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.seek finder (0, false, []) cmd_stack + try Stack.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) + 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; + 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); + buffer#remove_tag Tags.Script.processed ~start ~stop; + buffer#remove_tag Tags.Script.unjustified ~start ~stop; +(* buffer#remove_tag Tags.Script.tooltip ~start ~stop; *) + buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#move_mark ~where:start (`NAME "start_of_input") + end; + List.iter (fun { start } -> buffer#delete_mark start) seg; + List.iter (fun { stop } -> buffer#delete_mark stop) seg + (** Wrapper around the raw undo command *) method private backtrack_until ?(move_insert=true) until = let opening () = @@ -450,25 +563,28 @@ object(self) let conclusion () = pop_info (); if move_insert then buffer#place_cursor ~where:self#get_start_of_input; + let start = self#get_start_of_input in + let stop = self#get_end_of_input in + Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset); + buffer#remove_tag Tags.Script.error ~start ~stop; + buffer#remove_tag Tags.Script.error_bg ~start ~stop; + buffer#remove_tag Tags.Script.tooltip ~start ~stop; + buffer#remove_tag Tags.Script.processed ~start ~stop; + buffer#remove_tag Tags.Script.to_process ~start ~stop; self#show_goals in - let cleanup n l = - for i = 1 to n do ignore(Stack.pop cmd_stack) done; - if l <> [] then begin - let start = buffer#get_iter_at_mark (CList.hd l).start in - let stop = buffer#get_iter_at_mark (CList.last l).stop in - buffer#remove_tag Tags.Script.processed ~start ~stop; - buffer#remove_tag Tags.Script.unjustified ~start ~stop; -(* buffer#remove_tag Tags.Script.tooltip ~start ~stop; *) - buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#move_mark ~where:start (`NAME "start_of_input") - end; - List.iter (fun { start } -> buffer#delete_mark start) l; - List.iter (fun { stop } -> buffer#delete_mark stop) l in Coq.bind (Coq.lift opening) (fun () -> let rec undo until = let n, to_id, sentence, seg = self#segment_to_be_cleared until in - Coq.bind (Coq.backto to_id) (function - | Good () -> cleanup n seg; conclusion () + Coq.bind (Coq.edit_at to_id) (function + | Good (CSig.Inl (* NewTip *) ()) -> + self#cleanup n seg; + conclusion () + | Good (CSig.Inr (* Focus *) (stop_id,(start_id,tip))) -> + 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; + conclusion () | Fail (safe_id, loc, msg) -> if loc <> None then messages#push Error "Fixme LOC"; messages#push Error msg; @@ -485,14 +601,7 @@ object(self) messages#clear; messages#push Error msg; ignore(self#process_feedback ()); - let safe_flags s = s.flags = [ `UNSAFE ] || s.flags = [] in - let find_last_safe_id s = - match s.state_id with - | Some id -> safe_flags s | None -> false in - try - let last_safe = Stack.find find_last_safe_id cmd_stack in - self#backtrack_until (fun _ id _ _ -> id = last_safe.state_id) - with Not_found -> self#backtrack_until (fun _ id _ _ -> id = Some safe_id) + self#backtrack_until ~move_insert:false (fun _ id _ _ -> id = Some safe_id) method backtrack_last_phrase = let until n _ _ _ = n >= 1 in @@ -543,14 +652,14 @@ object(self) in let try_phrase phrase stop more = let action = log "Sending to coq now" in - let query = Coq.interp ~verbose:false 0 phrase in + let query = Coq.query (phrase,Stateid.dummy) in let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); messages#add ("Unsuccessfully tried: "^phrase); more - | Good (_, id) -> -(* messages#add msg; *) + | Good msg -> + messages#add msg; stop Tags.Script.processed in Coq.bind (Coq.seq action query) next @@ -566,6 +675,7 @@ 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 buffer#delete_mark phrase.start; @@ -573,6 +683,7 @@ object(self) done; (* reset the buffer *) buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input"); + buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input"); Sentence.tag_all buffer; (* clear the views *) messages#clear; @@ -604,12 +715,13 @@ object(self) | Good true -> Coq.return () | Good false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - let cmd = Coq.interp (hidden_edit_id ()) cmd in + let cmd = Coq.add ((cmd,hidden_edit_id ()),(Stateid.initial,false)) in let next = function | Fail (_, l, str) -> messages#set ("Couln't add loadpath:\n"^str); Coq.return () - | Good (id, _) -> initial_state <- id; Coq.return () + | Good (id, _) -> + initial_state <- id; Coq.return () in Coq.bind cmd next in diff --git a/ide/sentence.ml b/ide/sentence.ml index 01add490e..7b98d5296 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -14,7 +14,8 @@ an unterminated sentence. *) let split_slice_lax (buffer:GText.buffer) start stop = - List.iter (buffer#remove_tag ~start ~stop) Tags.Script.all; + buffer#remove_tag ~start ~stop Tags.Script.sentence; + buffer#remove_tag ~start ~stop Tags.Script.error; let slice = buffer#get_text ~start ~stop () in let apply_tag off tag = (* off is now a utf8-compliant char offset, cf Coq_lex.utf8_adjust *) @@ -98,14 +99,16 @@ let tag_on_insert buffer = found by [grab_ending_dot] to form a non-ending "..". In any case, we retag up to eof, since this isn't that costly. *) if not stop#is_end then - try split_slice_lax buffer start buffer#end_iter + let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in + try split_slice_lax buffer start eoi with Coq_lex.Unterminated -> () with StartError -> buffer#apply_tag ~start:soi ~stop:soi#forward_char Tags.Script.error let tag_all buffer = let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in - try split_slice_lax buffer soi buffer#end_iter + let eoi = buffer#get_iter_at_mark (`NAME "stop_of_input") in + try split_slice_lax buffer soi eoi with Coq_lex.Unterminated -> () (** Search a sentence around some position *) diff --git a/ide/session.ml b/ide/session.ml index e9d4b48ac..837674424 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -35,6 +35,8 @@ let create_buffer () = () in let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in + let _ = buffer#create_mark + ~left_gravity:false ~name:"stop_of_input" buffer#end_iter in let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in let _ = buffer#place_cursor ~where:buffer#start_iter in let _ = buffer#add_selection_clipboard Ideutils.cb in @@ -93,41 +95,75 @@ let set_buffer_handlers let call_coq_or_cancel_action f = Coq.try_grab coqtop f (fun () -> cancel_signal "Coq busy") in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in + let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in + let ensure_marks_exist () = + try ignore(buffer#get_mark (`NAME "stop_of_input")) + with GText.No_such_mark _ -> assert false in let get_insert () = buffer#get_iter_at_mark `INSERT in + let debug_edit_zone () = if !Minilib.debug then begin + buffer#remove_tag Tags.Script.edit_zone + ~start:buffer#start_iter ~stop:buffer#end_iter; + buffer#apply_tag Tags.Script.edit_zone + ~start:(get_start()) ~stop:(get_stop()) + end in + let backto_before_error it = + let rec aux old it = + if it#is_start || not(it#has_tag Tags.Script.error_bg) then old + else aux it it#backward_char in + aux it it in let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); let text_mark = add_mark it in if it#has_tag Tags.Script.to_process then - cancel_signal "Altering to the script being processed in not implemented" + cancel_signal "Altering the script being processed in not implemented" + else if it#has_tag Tags.Script.read_only then + cancel_signal "Altering read_only text not allowed" else if it#has_tag Tags.Script.processed then call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) - end in + else if it#has_tag Tags.Script.error_bg then begin + let prev_sentence_end = backto_before_error it in + let text_mark = add_mark prev_sentence_end in + call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) + end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); - let min_iter = if start#compare stop < 0 then start else stop in + cur_action := new_action_id (); + let min_iter, max_iter = + if start#compare stop < 0 then start, stop else stop, start in let text_mark = add_mark min_iter in - if min_iter#has_tag Tags.Script.to_process then - cancel_signal "Altering to the script being processed in not implemented" - else if min_iter#has_tag Tags.Script.processed then - call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) in + let rec aux min_iter = + if min_iter#equal max_iter then () + else if min_iter#has_tag Tags.Script.to_process then + cancel_signal "Altering the script being processed in not implemented" + else if min_iter#has_tag Tags.Script.read_only then + cancel_signal "Altering read_only text not allowed" + else if min_iter#has_tag Tags.Script.processed then + call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) + else if min_iter#has_tag Tags.Script.error_bg then + let prev_sentence_end = backto_before_error min_iter in + let text_mark = add_mark prev_sentence_end in + call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) + else aux min_iter#forward_char in + aux min_iter in let begin_action_cb () = + Minilib.log "begin_action_cb"; action_was_cancelled := false; let where = get_insert () in buffer#move_mark (`NAME "prev_insert") ~where in let end_action_cb () = Minilib.log "end_action_cb"; + ensure_marks_exist (); if not !action_was_cancelled then begin - Minilib.log "cleanup tags"; - let start = get_start () in - let stop = buffer#end_iter in - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; - buffer#remove_tag Tags.Script.tooltip ~start ~stop; - buffer#remove_tag Tags.Script.processed ~start ~stop; - buffer#remove_tag Tags.Script.to_process ~start ~stop; - Sentence.tag_on_insert buffer; + Sentence.tag_on_insert buffer end in + let mark_deleted_cb m = + match GtkText.Mark.get_name m with + | Some "insert" -> () + | Some s -> Minilib.log (s^" deleted") + | None -> () + in let mark_set_cb it m = + debug_edit_zone (); let ins = get_insert () in let line = ins#line + 1 in let off = ins#line_offset + 1 in @@ -144,6 +180,7 @@ let set_buffer_handlers let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in let _ = buffer#connect#end_user_action ~callback:end_action_cb in let _ = buffer#connect#after#mark_set ~callback:mark_set_cb in + let _ = buffer#connect#after#mark_deleted ~callback:mark_deleted_cb in () let create_proof () = diff --git a/ide/tags.ml b/ide/tags.ml index a91905dcd..de3287720 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -28,9 +28,19 @@ struct let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) + let all = [comment_sentence; error; error_bg; to_process; processed; unjustified; found; sentence; tooltip] + + let edit_zone = + let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in + t#set_priority (List.length all); + t + let all = edit_zone :: all + + let read_only = make_tag table ~name:"read_only" [`EDITABLE false ] + end module Proof = struct diff --git a/ide/tags.mli b/ide/tags.mli index ddd240d2a..f79ae1f11 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -18,7 +18,11 @@ sig val found : GText.tag val sentence : GText.tag val tooltip : GText.tag + val edit_zone : GText.tag (* for debugging *) val all : GText.tag list + + (* Not part of the all list. Special tags! *) + val read_only : GText.tag end module Proof : diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index a95b9f892..3422b1682 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -115,11 +115,11 @@ object(self) in let log level message = result#buffer#insert (message^"\n") in let process = - Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function + Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> result#buffer#insert str; Coq.return () - | Interface.Good (_,res) -> + | Interface.Good res -> result#buffer#insert res; Coq.return ()) in |