Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.

2 files changed, 4 insertions, 1 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b3694d0e98..11cb047e09 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,7 +27,7 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacTime l ->
+  | VernacRedirect (_, l) | VernacTime l ->
     List.exists
       (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f33c71d8a6..4300d5e244 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1849,6 +1849,7 @@ let interp ?proof locality poly c =
   | VernacLoad _ -> assert false
   | VernacFail _ -> assert false
   | VernacTime _ -> assert false
+  | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
   | VernacStm _ -> assert false
 
@@ -2127,6 +2128,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacTimeout (n,v) ->
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
+    | VernacRedirect (s, v) ->
+         Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v;
     | VernacTime v ->
         System.with_time !Flags.time
           (aux_list ?locality ?polymorphism isprogcmd) v;