aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml8
-rw-r--r--ide/coq.mli12
-rw-r--r--ide/coqOps.ml278
-rw-r--r--ide/sentence.ml9
-rw-r--r--ide/session.ml69
-rw-r--r--ide/tags.ml10
-rw-r--r--ide/tags.mli4
-rw-r--r--ide/wg_Command.ml4
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