aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml27
-rw-r--r--ide/coqide.ml5
-rw-r--r--ide/session.ml1
-rw-r--r--ide/tags.ml7
-rw-r--r--ide/tags.mli1
-rw-r--r--lib/interface.mli2
-rw-r--r--lib/serialize.ml4
-rw-r--r--toplevel/stm.ml3
8 files changed, 42 insertions, 8 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8b8f0791d9..ab70e35b98 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -11,15 +11,16 @@ open Coq
open Ideutils
open Interface
-type flag = [ `UNSAFE | `PROCESSING | `ERROR of string ]
-type mem_flag = [ `UNSAFE | `PROCESSING | `ERROR ]
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ]
+type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ]
let mem_flag_of_flag : flag -> mem_flag = function
| `ERROR _ -> `ERROR
- | (`UNSAFE | `PROCESSING) as mem_flag -> mem_flag
+ | (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
let str_of_flag = function
| `UNSAFE -> "U"
| `PROCESSING -> "P"
| `ERROR _ -> "E"
+ | `INCOMPLETE -> "I"
module SentenceId : sig
@@ -282,7 +283,9 @@ object(self)
let unjustified = Tags.Script.unjustified in
let error_bg = Tags.Script.error_bg in
let error = Tags.Script.error in
- let all_tags = [ error_bg; to_process; processed; unjustified; error ] in
+ let incomplete = Tags.Script.incomplete in
+ let all_tags = [
+ error_bg; to_process; incomplete; processed; unjustified; error ] in
let tags =
(if has_flag sentence `PROCESSING then to_process else
if has_flag sentence `ERROR then error_bg else
@@ -291,7 +294,9 @@ object(self)
(if [ `UNSAFE ] = sentence.flags then [unjustified] else [])
in
List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
- List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
+ List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags;
+ if has_flag sentence `INCOMPLETE then
+ buffer#apply_tag incomplete ~start ~stop
method private attach_tooltip sentence loc text =
let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
@@ -343,6 +348,14 @@ object(self)
remove_flag sentence `PROCESSING;
remove_flag sentence `ERROR;
self#mark_as_needed sentence
+ | Incomplete, Some (id, sentence) ->
+ log "Incomplete" id;
+ add_flag sentence `INCOMPLETE;
+ self#mark_as_needed sentence
+ | Complete, Some (id, sentence) ->
+ log "Complete" id;
+ remove_flag sentence `INCOMPLETE;
+ self#mark_as_needed sentence
| GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) ->
log "GlobRef" id;
self#attach_tooltip sentence loc
@@ -566,8 +579,9 @@ object(self)
let start = buffer#get_iter_at_mark (CList.last seg).start in
let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
Minilib.log
- (Printf.sprintf "Clean tags in range %d -> %d" start#offset stop#offset);
+ (Printf.sprintf "Cleanup in range %d -> %d" start#offset stop#offset);
buffer#remove_tag Tags.Script.processed ~start ~stop;
+ buffer#remove_tag Tags.Script.incomplete ~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;
@@ -590,6 +604,7 @@ object(self)
Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
+ buffer#remove_tag Tags.Script.incomplete ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
buffer#remove_tag Tags.Script.unjustified ~start ~stop;
self#show_goals in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b223be3a40..9da46d2e6a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1389,6 +1389,11 @@ let build_ui () =
(* Color configuration *)
Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
Tags.set_processed_color (Tags.color_of_string prefs.processed_color);
+ Tags.Script.incomplete#set_property
+ (`BACKGROUND_STIPPLE
+ (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
+ Tags.Script.incomplete#set_property
+ (`BACKGROUND_GDK (Tags.get_processed_color ()));
(* Showtime ! *)
w#show ()
diff --git a/ide/session.ml b/ide/session.ml
index ec5be3b29c..fe15ebb4bb 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -180,6 +180,7 @@ let set_buffer_handlers
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;
+ buffer#remove_tag Tags.Script.incomplete ~start ~stop;
Sentence.tag_on_insert buffer
end;
end in
diff --git a/ide/tags.ml b/ide/tags.ml
index 89675d8ef2..64eead294e 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -25,13 +25,17 @@ struct
let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
+ let incomplete = make_tag table ~name:"incomplete" [
+ `BACKGROUND !processing_color;
+ `BACKGROUND_STIPPLE_SET true;
+ ]
let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
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; error; error_bg; to_process; processed; unjustified;
+ [comment; error; error_bg; to_process; processed; incomplete; unjustified;
found; sentence; tooltip]
let edit_zone =
@@ -81,6 +85,7 @@ let get_processing_color () = color_of_string !processing_color
let set_processing_color clr =
let s = string_of_color clr in
processing_color := s;
+ Script.incomplete#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 e2447aabe2..8861703601 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -14,6 +14,7 @@ sig
val error_bg : GText.tag
val to_process : GText.tag
val processed : GText.tag
+ val incomplete : GText.tag
val unjustified : GText.tag
val found : GText.tag
val sentence : GText.tag
diff --git a/lib/interface.mli b/lib/interface.mli
index a01ec20aed..8d250f8507 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -127,6 +127,8 @@ type edit_or_state_id = Edit of edit_id | State of state_id
type feedback_content =
| AddedAxiom
| Processed
+ | Incomplete
+ | Complete
| GlobRef of Loc.t * string * string * string * string
| ErrorMsg of Loc.t * string
| InProgress of int
diff --git a/lib/serialize.ml b/lib/serialize.ml
index b1768d76dc..411fb9878e 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -328,6 +328,8 @@ let to_loc xml = match xml with
let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
| "addedaxiom", _ -> AddedAxiom
| "processed", _ -> Processed
+ | "incomplete", _ -> Incomplete
+ | "complete", _ -> Complete
| "globref", [loc; filepath; modpath; ident; ty] ->
GlobRef(to_loc loc, to_string filepath,
to_string modpath, to_string ident, to_string ty)
@@ -340,6 +342,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
let of_feedback_content = function
| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
| Processed -> constructor "feedback_content" "processed" []
+ | Incomplete -> constructor "feedback_content" "incomplete" []
+ | Complete -> constructor "feedback_content" "complete" []
| GlobRef(loc, filepath, modpath, ident, ty) ->
constructor "feedback_content" "globref" [
of_loc loc;
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index d05fce8b69..bca2ce24c5 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1139,7 +1139,8 @@ let known_state ?(redefine_qed=false) ~cache id =
qed.fproof <- Some (fp, cancel);
let proof = Proof_global.close_future_proof fp in
reach view.next;
- vernac_interp id ~proof x
+ vernac_interp id ~proof x;
+ feedback ~state_id:id Interface.Incomplete
| VtDrop, _, _ ->
reach view.next;
Option.iter (vernac_interp start) proof_using_ast;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 14:13:18 +0000