diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:47:52 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:57:45 +0200 |
commit | 20457cbff0b851ac9099847c91f74d48c5fe5be6 (patch) | |
tree | 6e3277c4fa6148303f6596e320b42bb94068722b /ide | |
parent | fe87c2cab20335b2d5dff61054700597e515f8a1 (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.ml | 30 | ||||
-rw-r--r-- | ide/coqide.ml | 5 | ||||
-rw-r--r-- | ide/session.ml | 4 | ||||
-rw-r--r-- | ide/tags.ml | 5 | ||||
-rw-r--r-- | ide/tags.mli | 3 |
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 : |