From 0e9161af86787d4f368554111001cab73bb7b323 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 4 Feb 2018 22:12:45 +0100 Subject: [toplevel] Refine start of interactive mode conditions. Refinement of the toplevel codepath requires to be more careful about the conditions for coqtop to be interactive. Fixes #6691. We also tweak the vio auxiliary function. --- toplevel/coqtop.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 572092e74..bf090862f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -424,12 +424,10 @@ let set_vio_checking_j opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 -let schedule_vio_checking () = - if !vio_files <> [] && !vio_checking then +let schedule_vio opts = + if !vio_checking then Vio_checking.schedule_vio_checking !vio_files_j !vio_files - -let schedule_vio_compilation () = - if !vio_files <> [] && not !vio_checking then + else Vio_checking.schedule_vio_compilation !vio_files_j !vio_files (******************************************************************************) @@ -840,7 +838,11 @@ let init_toplevel arglist = We split the codepath here depending whether coqtop is called in interactive mode or not. *) - if (not !batch_mode || CList.is_empty !compile_list) + (* The condition for starting the interactive mode is a bit + convoluted, we should really refactor batch/compilation_mode + more. *) + if (not !batch_mode + || CList.(is_empty !compile_list && is_empty !vio_files && is_empty !vio_tasks)) (* Interactive *) then begin try @@ -855,8 +857,9 @@ let init_toplevel arglist = end else begin try compile_files ~time:!measure_time; - schedule_vio_checking (); - schedule_vio_compilation (); + (* Vio compile pass *) + if !vio_files <> [] then schedule_vio (); + (* Vio task pass *) check_vio_tasks (); (* Allow the user to output an arbitrary state *) outputstate (); -- cgit v1.2.3