CoqIDE: new feedback "incomplete" to signal partial Qed

5 files changed, 34 insertions, 7 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