diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-04 22:12:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-05 02:48:20 +0100 |
| commit | 0e9161af86787d4f368554111001cab73bb7b323 (patch) | |
| tree | 8f139318f48160925104637dd03fec868b827c84 /toplevel | |
| parent | 76aff3cbe39da657abb1f559b8ba411a49aab317 (diff) | |
[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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 19 |
1 files changed, 11 insertions, 8 deletions
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 (); |