aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-04-02 15:47:52 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-04-02 15:57:45 +0200
commit20457cbff0b851ac9099847c91f74d48c5fe5be6 (patch)
tree6e3277c4fa6148303f6596e320b42bb94068722b /ide
parentfe87c2cab20335b2d5dff61054700597e515f8a1 (diff)
CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)
No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch.
Diffstat (limited to 'ide')
-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
5 files changed, 11 insertions, 36 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 :