option for displaying labels

src/ide/gconfig.ml

@@ -45,6 +45,7 @@ type t =
       mutable max_running_processes : int;
       mutable provers : prover_data Util.Mstr.t;
       mutable default_editor : string;
+      mutable show_labels : bool;
       mutable env : Env.env;
       mutable config : Whyconf.config;
     }
@@ -128,6 +129,7 @@ let load_config config =
 *)
     provers = Mstr.empty;
     default_editor = ide.ide_default_editor;
+    show_labels = false;
     config         = config;
     env            = env
   }
@@ -327,6 +329,11 @@ let show_about_window () =
   let ( _ : GWindow.Buttons.about) = about_dialog#run () in
   about_dialog#destroy ()
 
+let set_labels_flag = 
+  let fl = Debug.lookup_flag "print_labels" in
+  fun b ->
+    (if b then Debug.set_flag else Debug.unset_flag) fl
+
 let preferences c =
   let dialog = GWindow.dialog ~title:"Why: preferences" () in
   let vbox = dialog#vbox in
@@ -337,6 +344,16 @@ let preferences c =
     GPack.vbox ~homogeneous:false ~packing:
       (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
   in
+  (* toggle show labels in formulas *)
+  let showlabels =
+    GButton.check_button ~label:"show labels in formulas" ~packing:page1#add ()
+      ~active:(set_labels_flag c.show_labels;c.show_labels)
+  in
+  let (_ : GtkSignal.id) =
+    showlabels#connect#toggled ~callback:
+      (fun () -> c.show_labels <- not c.show_labels;
+         set_labels_flag c.show_labels)
+  in
   (* editor *)
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
  let _ = GMisc.label ~text:"Default editor" ~packing:hb#add () in

src/ide/gconfig.mli

@@ -40,6 +40,7 @@ type t =
       mutable max_running_processes : int;
       mutable provers : prover_data Util.Mstr.t;
       mutable default_editor : string;
+      mutable show_labels : bool;
       mutable env : Why.Env.env;
       mutable config : Whyconf.config;
     }

src/programs/pgm_wp.ml

@@ -330,8 +330,9 @@ and wp_desc env e q = match e.expr_desc with
 	| Some i ->
 	    wp_and wfr
 	      (wp_and ~sym:true
-		 i
-		 (quantify env e.expr_effect (wp_implies i we)))
+		 (f_label_add (label "LoopInvInit") i)
+                 (f_label_add (label "LoopInvPres")
+		    (quantify env e.expr_effect (wp_implies i we))))
 	in
 	w
   (* optimization for the particular case let _ = y in e *)
@@ -417,10 +418,10 @@ and wp_desc env e q = match e.expr_desc with
 
   | Eassert (Ptree.Aassert, f) ->
       let (_, q), _ = q in
-      wp_and f q
+      wp_and (f_label_add (label "Assert") f) q
   | Eassert (Ptree.Acheck, f) ->
       let (_, q), _ = q in
-      wp_and ~sym:true f q
+      wp_and ~sym:true (f_label_add (label "Check") f) q
   | Eassert (Ptree.Aassume, f) ->
       let (_, q), _ = q in
       wp_implies f q