diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-25 11:02:43 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 45d6972565c82ddd9b7aae92f2928d500a6fc228 (patch) | |
| tree | 36359aa8461bb116f29a2117fa1be66208c65cd5 /toplevel/coqtop.ml | |
| parent | 15b6c9b6fa268a9af6dd4f05961e469545e92a6f (diff) | |
vi2vo: new flag -schedule-vi2vo
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8a133fc48..d2f680d6e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -262,7 +262,7 @@ let check_vi_tasks () = let vi_files = ref [] let vi_files_j = ref 0 - +let vi_checking = ref false let add_vi_file f = set_batch_mode (); Flags.make_silent true; @@ -273,7 +273,7 @@ let set_vi_checking_j opt j = prerr_endline ("The first argument of " ^ opt ^ " must the number"); prerr_endline "of concurrent workers to be used (a positive integer)."; prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make checkproofs J=3'"; + prerr_endline "setting the J variable like in 'make vi2vo J=3'"; exit 1 let is_not_dash_option = function @@ -281,8 +281,11 @@ let is_not_dash_option = function | _ -> false let schedule_vi_checking () = - if !vi_files <> [] then + if !vi_files <> [] && !vi_checking then Vi_checking.schedule_vi_checking !vi_files_j !vi_files +let schedule_vi_compilation () = + if !vi_files <> [] && not !vi_checking then + Vi_checking.schedule_vi_compilation !vi_files_j !vi_files let parse_args arglist = let args = ref arglist in @@ -323,6 +326,11 @@ let parse_args arglist = let tfile = next () in add_vi_task (tno,tfile) |"-schedule-vi-checking" -> + vi_checking := true; + set_vi_checking_j opt (next ()); + add_vi_file (next ()); + while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done + |"-schedule-vi2vo" -> set_vi_checking_j opt (next ()); add_vi_file (next ()); while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done @@ -466,6 +474,7 @@ let init arglist = load_vernacular (); compile_files (); schedule_vi_checking (); + schedule_vi_compilation (); check_vi_tasks (); outputstate () with any -> |