diff options
| author | Maxime Dénès | 2019-02-04 13:05:00 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-04 13:05:00 +0100 |
| commit | 129d47518ae950c6ef1b69763e93cd70c14863f6 (patch) | |
| tree | e5ae9646636c50f07c3b60e08eccb76e5b6eff96 /vernac | |
| parent | 0be49a49c41e28b2015440723882e0ca15c02d5e (diff) | |
| parent | 103f59ed6b8174ed9359cb11c909f1b2219390c9 (diff) | |
Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.
Reviewed-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/topfmt.ml | 5 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 1 |
2 files changed, 5 insertions, 1 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b4b893a3fd..ed93267665 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -335,6 +335,7 @@ type execution_phase = | LoadingPrelude | LoadingRcFile | InteractiveLoop + | CompilationPhase let default_phase = ref InteractiveLoop @@ -373,7 +374,9 @@ let pr_phase ?loc () = Some (str "While loading initial state:" ++ Option.cata (fun loc -> fnl () ++ pr_loc loc) (mt ()) loc) | _, Some loc -> Some (pr_loc loc) | ParsingCommandLine, _ - | Initialization, _ -> None + | Initialization, _ + | CompilationPhase, _ -> + None | InteractiveLoop, _ -> (* Note: interactive messages such as "foo is defined" are not located *) None diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 5f84c5edee..b0e3b3772c 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -60,6 +60,7 @@ type execution_phase = | LoadingPrelude | LoadingRcFile | InteractiveLoop + | CompilationPhase val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b |