diff options
| author | Hugo Herbelin | 2018-11-19 15:45:46 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:19 +0000 |
| commit | 390e8b97482a3100e8d37e2e62a345f9267960e2 (patch) | |
| tree | 0d7a0f2c21b383529c91146f7a97f45ead09912d /ide | |
| parent | ab276ee0e26c52e9ee049077e95e2454b17da203 (diff) | |
CoqIDE: Stippling using bitmap no more supported for incomplete Qed.
Was formerly displaying a stippled ("pointillé") light blue. Now only
a light blue.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/tags.ml | 2 |
2 files changed, 1 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 4b08a8795c..386bd8047c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1303,11 +1303,6 @@ let build_ui () = let _ = source_style#connect#changed ~callback:refresh_style in let _ = source_language#connect#changed ~callback:refresh_language in - (* Color configuration *) - Tags.Script.incomplete#set_property - (`BACKGROUND_STIPPLE - (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); - (* Showtime ! *) w#show (); w diff --git a/ide/tags.ml b/ide/tags.ml index 60195e8acb..e919a64278 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -24,7 +24,7 @@ struct let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] - let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true] + let incomplete = make_tag table ~name:"incomplete" [] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) let ephemere = |