aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
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 c6073d599d..af728471f7 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 87efd17d22..eb994fe8e8 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 e0466b7e3a..12b7796633 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 d4460b0770..c9b57af4cb 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 e68015c991..14cfd0dbfe 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 :
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 22:57:18 +0000