diff options
| -rw-r--r-- | interp/dumpglob.ml | 26 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 1 | ||||
| -rw-r--r-- | lib/interface.mli | 1 | ||||
| -rw-r--r-- | lib/serialize.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 7 | ||||
| -rw-r--r-- | toplevel/stm.ml | 2 |
6 files changed, 33 insertions, 12 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 3baa4d011..ca5b0eddd 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -22,6 +22,7 @@ type glob_output_t = | NoGlob | StdOut | MultFiles + | Feedback | File of string let glob_output = ref NoGlob @@ -38,8 +39,11 @@ let dump_into_file f = else (glob_output := File f; open_glob_file f) +let feedback_glob () = glob_output := Feedback + let dump_string s = - if dump () then Pervasives.output_string !glob_file s + if dump () && !glob_output != Feedback then + Pervasives.output_string !glob_file s let start_dump_glob vfile = match !glob_output with @@ -51,13 +55,13 @@ let start_dump_glob vfile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | StdOut -> + | NoGlob | Feedback | StdOut -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | StdOut -> () + | NoGlob | Feedback | StdOut -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob @@ -126,8 +130,11 @@ let interval loc = loc1, loc2-1 let dump_ref loc filepath modpath ident ty = - let bl,el = interval loc in - dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" + if !glob_output = Feedback then + Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty)) + else + let bl,el = interval loc in + dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el filepath modpath ident ty) let dump_reference loc modpath ident ty = @@ -220,9 +227,12 @@ let add_glob_kn loc kn = let dump_binding loc id = () -let dump_definition (loc, id) sec s = - let bl,el = interval loc in - dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) +let dump_def ty loc secpath id = + if !glob_output = Feedback then + Pp.feedback (Interface.GlobDef (loc, id, secpath, ty)) + else + let bl,el = interval loc in + dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) let dump_definition (loc, id) sec s = dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 37370f6e1..28ada9fd9 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -17,6 +17,7 @@ val dump : unit -> bool val noglob : unit -> unit val dump_into_file : string -> unit (** special handling of "stdout" *) val dump_to_dotglob : unit -> unit +val feedback_glob : unit -> unit val pause : unit -> unit val continue : unit -> unit diff --git a/lib/interface.mli b/lib/interface.mli index 8af26196c..c8fe068e6 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -130,6 +130,7 @@ type feedback_content = | Incomplete | Complete | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string | InProgress of int | SlaveStatus of int * string diff --git a/lib/serialize.ml b/lib/serialize.ml index d91f736fd..c97817779 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -323,6 +323,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "globref", [loc; filepath; modpath; ident; ty] -> GlobRef(to_loc loc, to_string filepath, to_string modpath, to_string ident, to_string ty) + | "globdef", [loc; ident; secpath; ty] -> + GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) | "slavestatus", [ns] -> @@ -342,6 +344,12 @@ let of_feedback_content = function of_string modpath; of_string ident; of_string ty ] + | GlobDef(loc, ident, secpath, ty) -> + constructor "feedback_content" "globdef" [ + of_loc loc; + of_string ident; + of_string secpath; + of_string ty ] | ErrorMsg(loc, s) -> constructor "feedback_content" "errormsg" [of_loc loc; of_string s] | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bf0c872cc..954d75493 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 19249320b..fc52d3644 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" |