[ide] highlighting, distinguishes positive and negative premises (contribution by AstraVer project)

src/ide/gconfig.ml

@@ -46,6 +46,7 @@ type t =
       mutable saving_policy : int;
       (** 0 = always, 1 = never, 2 = ask *)
       mutable premise_color : string;
+      mutable neg_premise_color : string;
       mutable goal_color : string;
       mutable error_color : string;
       mutable iconset : string;
@@ -77,6 +78,7 @@ type ide = {
   ide_max_boxes : int;
   ide_saving_policy : int;
   ide_premise_color : string;
+  ide_neg_premise_color : string;
   ide_goal_color : string;
   ide_error_color : string;
   ide_iconset : string;
@@ -100,6 +102,7 @@ let default_ide =
     ide_max_boxes = 16;
     ide_saving_policy = 2;
     ide_premise_color = "chartreuse";
+    ide_neg_premise_color = "pink";
     ide_goal_color = "gold";
     ide_error_color = "orange";
     ide_iconset = "fatcow";
@@ -141,6 +144,9 @@ let load_ide section =
     ide_premise_color =
       get_string section ~default:default_ide.ide_premise_color
         "premise_color";
+    ide_neg_premise_color =
+      get_string section ~default:default_ide.ide_neg_premise_color
+        "neg_premise_color";
     ide_goal_color =
       get_string section ~default:default_ide.ide_goal_color
         "goal_color";
@@ -191,6 +197,7 @@ let load_config config original_config env =
     max_boxes = ide.ide_max_boxes;
     saving_policy = ide.ide_saving_policy ;
     premise_color = ide.ide_premise_color;
+    neg_premise_color = ide.ide_neg_premise_color;
     goal_color = ide.ide_goal_color;
     error_color = ide.ide_error_color;
     iconset = ide.ide_iconset;
@@ -234,6 +241,7 @@ let save_config t =
   let ide = set_int ide "max_boxes" t.max_boxes in
   let ide = set_int ide "saving_policy" t.saving_policy in
   let ide = set_string ide "premise_color" t.premise_color in
+  let ide = set_string ide "neg_premise_color" t.neg_premise_color in
   let ide = set_string ide "goal_color" t.goal_color in
   let ide = set_string ide "error_color" t.error_color in
   let ide = set_string ide "iconset" t.iconset in

src/ide/gconfig.mli

@@ -27,6 +27,7 @@ type t =
       mutable max_boxes : int;
       mutable saving_policy : int;
       mutable premise_color : string;
+      mutable neg_premise_color : string;
       mutable goal_color : string;
       mutable error_color : string;
       mutable iconset : string;

src/ide/gmain.ml

@@ -1938,6 +1938,9 @@ let move_to_line ~yalign (v : GSourceView2.source_view) line =
 let premise_tag = source_view#buffer#create_tag
   ~name:"premise_tag" [`BACKGROUND gconfig.premise_color]
 
+let neg_premise_tag = source_view#buffer#create_tag
+  ~name:"neg_premise_tag" [`BACKGROUND gconfig.neg_premise_color]
+
 let goal_tag = source_view#buffer#create_tag
   ~name:"goal_tag" [`BACKGROUND gconfig.goal_color]
 
@@ -1947,6 +1950,7 @@ let error_tag = source_view#buffer#create_tag
 let erase_color_loc (v:GSourceView2.source_view) =
   let buf = v#buffer in
   buf#remove_tag premise_tag ~start:buf#start_iter ~stop:buf#end_iter;
+  buf#remove_tag neg_premise_tag ~start:buf#start_iter ~stop:buf#end_iter;
   buf#remove_tag goal_tag ~start:buf#start_iter ~stop:buf#end_iter;
   buf#remove_tag error_tag ~start:buf#start_iter ~stop:buf#end_iter
 
@@ -2001,13 +2005,17 @@ let rec color_locs ~color f =
 (* FIXME: we shouldn't open binders _every_time_ we redraw screen!!!
    No t_fold, no t_open_quant! *)
 let rec color_t_locs f =
+  let premise_tag = function
+    | { Term. t_node = Term.Tnot _; t_loc = None } -> neg_premise_tag
+    | _ -> premise_tag
+  in
   match f.Term.t_node with
     | Term.Tbinop (Term.Timplies,f1,f2) ->
-        let b = color_locs ~color:premise_tag f1 in
+        let b = color_locs ~color:(premise_tag f1) f1 in
         color_t_locs f2 || b
     | Term.Tlet (t,fb) ->
         let _,f1 = Term.t_open_bound fb in
-        let b = color_locs ~color:premise_tag t in
+        let b = color_locs ~color:(premise_tag t) t in
         color_t_locs f1 || b
     | Term.Tquant (Term.Tforall,fq) ->
         let _,_,f1 = Term.t_open_quant fq in