aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2013-12-24 18:12:26 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2013-12-24 18:23:41 +0100
commit7a7dd14e763d13887101834fc2288046740cb8a2 (patch)
treefe37d183be114e7b907629d60fb9d9ee7efb0683 /ide/coqide.ml
parent29969434c2b5625273e742d01cd7662c9db47d11 (diff)
CoqIDE: new feedback "incomplete" to signal partial Qed
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b223be3a4..9da46d2e6 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 ()