diff options
| author | Carst Tankink | 2014-04-10 12:33:42 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-04-10 19:43:08 +0200 |
| commit | f15525ac29af29bedbb04ae12297d67be3ce6475 (patch) | |
| tree | 45936c39365bf3170b4582610b45931c7b46c39e /toplevel | |
| parent | 546d47608f944d9463aaf49ec00dee026fe32818 (diff) | |
Have the feedback bus as a backend for dumping globs.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 7 | ||||
| -rw-r--r-- | toplevel/stm.ml | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bf0c872cc3..954d754937 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -348,6 +348,7 @@ let parse_args arglist = |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true + |"-feedback-glob" -> Dumpglob.feedback_glob () |"-exclude-dir" -> exclude_search_in_dirname (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) @@ -500,14 +501,14 @@ let start () = let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in (* In batch mode, Coqtop has already exited at this point. In interactive one, dump glob is nothing but garbage ... *) - let () = if Dumpglob.dump () then - let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in - Dumpglob.noglob () in if !Flags.ide_slave then Ide_slave.loop () else if Flags.async_proofs_is_worker () then Stm.slave_main_loop () else + let () = if Dumpglob.dump () then + let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in + Dumpglob.noglob () in Coqloop.loop(); (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 19249320bc..fc52d36443 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -928,7 +928,7 @@ end = struct (* {{{ *) let rec manage_slave ~cancel:cancel_user_req id_slave respawn = let ic, oc, proc = let rec set_slave_opt = function - | [] -> ["-async-proofs"; "worker"; string_of_int id_slave] + | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"] | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl | ("-async-proofs" |"-compile" |