aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml30
-rw-r--r--ide/coqide.ml5
-rw-r--r--ide/session.ml4
-rw-r--r--ide/tags.ml5
-rw-r--r--ide/tags.mli3
-rw-r--r--stm/stm.ml29
6 files changed, 29 insertions, 47 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c6073d599..af728471f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -276,21 +276,11 @@ object(self)
Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
self#print_stack;
let qed_s = Doc.tip_data document 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 =
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;
begin try
@@ -515,7 +505,7 @@ object(self)
| Some (start, stop) ->
if until n start stop then begin
()
- end else if start#has_tag Tags.Script.processed then begin
+ end else if stop#backward_char#has_tag Tags.Script.processed then begin
Queue.push (`Skip (start, stop)) queue;
loop n stop
end else begin
@@ -563,12 +553,15 @@ object(self)
script#recenter_insert;
match topstack with
| [] -> self#show_goals_aux ?move_insert ()
- | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
+ | (_,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), [] ->
+ logger Pp.Error "You muse close the proof with Qed or Admitted";
+ self#discard_command_queue queue;
+ conclude []
| `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));
@@ -589,7 +582,7 @@ object(self)
Doc.assign_tip_id document id;
let topstack, _ = Doc.context document in
self#exit_focus;
- self#cleanup ~all:true (Doc.cut_at document tip);
+ self#cleanup (Doc.cut_at document tip);
logger Pp.Notice msg;
self#mark_as_needed sentence;
if Queue.is_empty queue then loop tip []
@@ -651,7 +644,7 @@ object(self)
Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
with Not_found -> initial_state, Doc.focused document
- method private cleanup ~all seg =
+ method private cleanup seg =
if seg <> [] then begin
let start = buffer#get_iter_at_mark (CList.last seg).start in
let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
@@ -662,7 +655,6 @@ object(self)
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;
- if all then buffer#remove_tag Tags.Script.read_only ~start ~stop;
buffer#remove_tag Tags.Script.error ~start ~stop;
buffer#remove_tag Tags.Script.error_bg ~start ~stop;
buffer#move_mark ~where:start (`NAME "start_of_input")
@@ -694,13 +686,13 @@ object(self)
Coq.bind (Coq.edit_at to_id) (function
| Good (CSig.Inl (* NewTip *) ()) ->
if unfocus_needed then self#exit_focus;
- self#cleanup ~all:true (Doc.cut_at document to_id);
+ 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;
- self#cleanup ~all:true (Doc.cut_at document tip);
+ self#cleanup (Doc.cut_at document tip);
self#enter_focus start_id stop_id;
- self#cleanup ~all:false (Doc.cut_at document to_id);
+ self#cleanup (Doc.cut_at document to_id);
conclusion ()
| Fail (safe_id, loc, msg) ->
if loc <> None then messages#push Pp.Error "Fixme LOC";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 87efd17d2..eb994fe8e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1339,11 +1339,6 @@ let build_ui () =
(Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
Tags.Script.incomplete#set_property
(`BACKGROUND_GDK (Tags.get_processed_color ()));
- Tags.Script.read_only#set_property
- (`BACKGROUND_STIPPLE
- (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
- Tags.Script.read_only#set_property
- (`BACKGROUND_GDK (Tags.get_processed_color ()));
(* Showtime ! *)
w#show ()
diff --git a/ide/session.ml b/ide/session.ml
index e0466b7e3..12b779663 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -156,8 +156,6 @@ let set_buffer_handlers
let () = update_prev it in
if it#has_tag Tags.Script.to_process then
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))
else if it#has_tag Tags.Script.error_bg then begin
@@ -175,8 +173,6 @@ let set_buffer_handlers
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
diff --git a/ide/tags.ml b/ide/tags.ml
index d4460b077..c9b57af4c 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -52,10 +52,6 @@ struct
t
let all = edit_zone :: all
- let read_only = make_tag table ~name:"read_only" [`EDITABLE false;
- `BACKGROUND !processing_color;
- `BACKGROUND_STIPPLE_SET true ]
-
end
module Proof =
struct
@@ -96,7 +92,6 @@ let set_processing_color clr =
let s = string_of_color clr in
processing_color := s;
Script.incomplete#set_property (`BACKGROUND s);
- Script.read_only#set_property (`BACKGROUND s);
Script.to_process#set_property (`BACKGROUND s)
let get_error_color () = color_of_string !error_color
diff --git a/ide/tags.mli b/ide/tags.mli
index e68015c99..14cfd0dbf 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -21,9 +21,6 @@ sig
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/stm/stm.ml b/stm/stm.ml
index 477ca1f0d..38745e227 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -131,7 +131,7 @@ type cancel_switch = bool ref
type branch_type =
[ `Master
| `Proof of proof_mode * depth
- | `Edit of proof_mode * Stateid.t * Stateid.t ]
+ | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type ]
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
cast : ast;
@@ -449,7 +449,7 @@ end = struct (* {{{ *)
if List.mem edit_branch (Vcs_.branches !vcs) then begin
checkout edit_branch;
match get_branch edit_branch with
- | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+ | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
| _ -> assert false
end else
let pl = proof_nesting () in
@@ -1787,8 +1787,15 @@ let known_state ?(redefine_qed=false) ~cache id =
VCS.create_cluster nodes ~qed:id ~start;
begin match brinfo, qed.fproof with
| { VCS.kind = `Edit _ }, None -> assert false
- | { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
+ | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) ->
assert(redefine_qed = true);
+ if okeep != keep then
+ msg_error(strbrk("The command closing the proof changed. "
+ ^"The kernel cannot take this into account and will "
+ ^(if keep == VtKeep then "not check " else "reject ")
+ ^"the "^(if keep == VtKeep then "new" else "incomplete")
+ ^" proof. Reprocess the command declaring "
+ ^"the proof's statement to avoid that."));
let fp, cancel =
Slaves.build_proof
~loc ~drop_pt ~exn_info ~start ~stop ~name in
@@ -1914,7 +1921,7 @@ let finish ?(print_goals=false) () =
VCS.print ();
(* Some commands may by side effect change the proof mode *)
match VCS.get_branch head with
- | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+ | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
| { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
| _ -> ()
@@ -1982,7 +1989,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
VCS.delete_branch brname;
if keep <> VtDrop then VCS.propagate_sideff None;
`Ok
- | { VCS.kind = `Edit (mode, qed_id, master_id) } ->
+ | { VCS.kind = `Edit (mode, qed_id, master_id, _) } ->
let ofp =
match VCS.visit qed_id with
| { step = `Qed ({ fproof }, _) } -> fproof
@@ -2136,9 +2143,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
| { VCS.root; kind = `Proof(_,d); pos } ->
VCS.delete_branch bn;
VCS.branch ~root ~pos bn (`Proof(mode,d))
- | { VCS.root; kind = `Edit(_,f,q); pos } ->
+ | { VCS.root; kind = `Edit(_,f,q,k); pos } ->
VCS.delete_branch bn;
- VCS.branch ~root ~pos bn (`Edit(mode,f,q)))
+ VCS.branch ~root ~pos bn (`Edit(mode,f,q,k)))
(VCS.branches ());
VCS.checkout_shallowest_proof_branch ();
Backtrack.record ();
@@ -2291,13 +2298,13 @@ let edit_at id =
| { step = `Sideff (`Ast(_,id)|`Id id) } -> id
| { next } -> master_for_br root next in
let reopen_branch start at_id mode qed_id tip =
- let master_id, cancel_switch =
+ let master_id, cancel_switch, keep =
(* Hum, this should be the real start_id in the clusted and not next *)
match VCS.visit qed_id with
- | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs
+ | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
| _ -> anomaly (str "Cluster not ending with Qed") in
VCS.branch ~root:master_id ~pos:id
- VCS.edit_branch (`Edit (mode, qed_id, master_id));
+ VCS.edit_branch (`Edit (mode, qed_id, master_id, keep));
VCS.delete_cluster_of id;
cancel_switch := true;
Reach.known_state ~cache:(interactive ()) id;
@@ -2324,7 +2331,7 @@ let edit_at id =
let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
let branch_info =
match snd (VCS.get_info id).vcs_backup with
- | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m
+ | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m
| _ -> None in
match focused, VCS.cluster_of id, branch_info with
| _, Some _, None -> assert false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 20:47:54 +0000