Processing the task for counter-example also when editing the proof.

src/driver/driver.ml

@@ -277,7 +277,16 @@ let update_task = let ht = Hint.create 5 in fun drv ->
       add_tdecl task goal
   | task -> update task
 
-let prepare_task drv task =
+let add_cntexample_meta task cntexample =
+  if not (cntexample) then task
+  else
+    let cnt_meta = lookup_meta "get_counterexmp" in
+    let g,task = Task.task_separate_goal task in
+    let task = Task.add_meta task cnt_meta [] in
+    Task.add_tdecl task g
+
+let prepare_task ~cntexample drv task =
+  let task = add_cntexample_meta task cntexample in
   let lookup_transform t = lookup_transform t drv.drv_env in
   let transl = List.map lookup_transform drv.drv_transform in
   let apply task tr = Trans.apply tr task in
@@ -299,14 +308,14 @@ let print_task_prepared ?old drv fmt task =
   fprintf fmt "@[%a@]@?" (printer ?old) task;
   printer_args.printer_mapping
 
-let print_task ?old drv fmt task =
-  let task = prepare_task drv task in
+let print_task ?old ~cntexample drv fmt task =
+  let task = prepare_task ~cntexample drv task in
   let _ = print_task_prepared ?old drv fmt task in
   ()
 
 let print_theory ?old drv fmt th =
   let task = Task.use_export None th in
-  print_task ?old drv fmt task
+  print_task ?old ~cntexample:false drv fmt task
 
 let prove_task_prepared
     ~command ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
@@ -332,17 +341,8 @@ let prove_task_prepared
   Buffer.reset buf;
   res
 
-let add_cntexample_meta task cntexample =
-  if not (cntexample) then task
-  else
-    let cnt_meta = lookup_meta "get_counterexmp" in
-    let g,task = Task.task_separate_goal task in
-    let task = Task.add_meta task cnt_meta [] in
-    Task.add_tdecl task g
-
 let prove_task ~command ?(cntexample=false) ?timelimit ?memlimit ?steplimit ?old ?inplace drv task =
-  let task = add_cntexample_meta task cntexample in
-  let task = prepare_task drv task in
+  let task = prepare_task ~cntexample drv task in
   prove_task_prepared ~command ?timelimit ?memlimit
                       ?steplimit ?old ?inplace drv task
 

src/driver/driver.mli

@@ -47,6 +47,7 @@ val call_on_buffer :
 
 val print_task :
   ?old       : in_channel ->
+  cntexample : bool ->
   driver -> Format.formatter -> Task.task -> unit
 
 val print_theory :
@@ -65,7 +66,7 @@ val prove_task :
   driver -> Task.task -> Call_provers.pre_prover_call
 
 (** Split the previous function in two simpler functions *)
-val prepare_task : driver -> Task.task -> Task.task
+val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
 
 val print_task_prepared :
   ?old       : in_channel ->

src/ide/gmain.ml

@@ -2141,7 +2141,7 @@ let edit_selected_row r =
           "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
           0 time p.editor;
 *)
-        M.edit_proof e sched ~default_editor:gconfig.default_editor a
+        M.edit_proof ~cntexample:!opt_cntexmp e sched ~default_editor:gconfig.default_editor a
     | S.Transf _ -> ()
     | S.Metas _ -> ()
 

src/session/session.ml

@@ -1968,7 +1968,7 @@ let copy_external_proof
 
 exception UnloadableProver of Whyconf.prover
 
-let update_edit_external_proof env_session a =
+let update_edit_external_proof ~cntexample env_session a =
   let prover_conf = match load_prover env_session a.proof_prover with
     | Some prover_conf -> prover_conf
     | None -> raise (UnloadableProver a.proof_prover) in
@@ -2005,7 +2005,7 @@ let update_edit_external_proof env_session a =
   in
   let ch = open_out file in
   let fmt = formatter_of_out_channel ch in
-  Driver.print_task ?old driver fmt goal;
+  Driver.print_task ~cntexample ?old driver fmt goal;
   Opt.iter close_in old;
   close_out ch;
   file

src/session/session.mli

@@ -374,7 +374,7 @@ val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
 (** return the edited filename after concatenation to [session_dir] *)
 
 val update_edit_external_proof :
-  'key env_session -> 'key proof_attempt -> string
+  cntexample:bool -> 'key env_session -> 'key proof_attempt -> string
 (** return the absolute path of the edited file update with the
     current goal *)
 

src/session/session_scheduler.ml

@@ -831,7 +831,7 @@ let rec transform eS sched ~context_unproved_goals_only ?callback tr a =
 (* method: edit current goal *)
 (*****************************)
 
-let edit_proof_v3 eS sched ~default_editor callback a =
+let edit_proof_v3 ~cntexample eS sched ~default_editor callback a =
   match find_prover eS a with
   | None ->
           (* nothing to do
@@ -849,12 +849,12 @@ let edit_proof_v3 eS sched ~default_editor callback a =
                               ed.Whyconf.editor_options)
         with Not_found -> default_editor
     in
-    let file = update_edit_external_proof eS a in
+    let file = update_edit_external_proof ~cntexample eS a in
     Debug.dprintf debug "[Editing] goal %s with command '%s' on file %s@."
       a.proof_parent.goal_name.Ident.id_string editor file;
     schedule_edition sched editor file (fun res -> callback a res)
 
-let edit_proof eS sched ~default_editor a =
+let edit_proof ~cntexample eS sched ~default_editor a =
   (* check that the state is not Scheduled or Running *)
   if a.proof_archived || running a.proof_state then ()
 (*
@@ -870,16 +870,16 @@ let edit_proof eS sched ~default_editor a =
         set_proof_state ~notify ~obsolete:false ~archived:false
           res a
     in
-    edit_proof_v3 eS sched ~default_editor callback a
+    edit_proof_v3 ~cntexample eS sched ~default_editor callback a
 
-let edit_proof_v3 eS sched ~default_editor ~callback a =
+let edit_proof_v3 ~cntexample eS sched ~default_editor ~callback a =
   let callback a res =
     match res with
     | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
       callback a
     | _ -> ()
   in
-  edit_proof_v3 eS sched ~default_editor callback a
+  edit_proof_v3 ~cntexample eS sched ~default_editor callback a
 
 
 (*************)

src/session/session_scheduler.mli

@@ -231,12 +231,14 @@ module Make(O: OBSERVER) : sig
         must be applied also on alreadt proved goals *)
 
   val edit_proof :
+    cntexample:bool ->
     O.key env_session -> t ->
     default_editor:string ->
     O.key proof_attempt -> unit
   (** edits the given proof attempt using the appropriate editor *)
 
   val edit_proof_v3 :
+    cntexample:bool ->
     O.key env_session -> t ->
     default_editor:string ->
     callback:(O.key Session.proof_attempt ->  unit) ->

src/tools/why3prove.ml

@@ -284,7 +284,7 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
           (task_goal task).Decl.pr_name.Ident.id_string
           Call_provers.print_prover_result res
     | None, None ->
-        Driver.print_task drv std_formatter task
+        Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
     | Some dir, _ -> output_task drv fname tname th task dir
 
 let do_tasks env drv fname tname th task =

src/why3session/why3session_run.ml

@@ -309,6 +309,7 @@ let run_one sched env config filters interactive_provers fname =
               env_session sched pa 
 	      callback in
           M.edit_proof_v3 env_session sched
+	    ~cntexample:false
             ~default_editor:"" (** TODO? *)
             ~callback:callback_edit a 
         else