diff options
| author | Clément Pit--Claudel | 2015-04-23 01:14:49 -0400 |
|---|---|---|
| committer | Enrico Tassi | 2015-05-04 13:17:23 +0200 |
| commit | 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d (patch) | |
| tree | f23c8dc1ce9238ebf5cb05f61f57aa21dd8ee8ca /stm | |
| parent | f19d0c7baf91fb410de77baed391b0a16db9c4e2 (diff) | |
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.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 3 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
3 files changed, 6 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index f36b757f29..9771564752 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el + | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el | _ -> false in if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -1472,7 +1472,7 @@ end = struct (* {{{ *) let e, etac, time, fail = let rec find time fail = function | VernacSolve(_,_,re,b) -> re, b, time, fail - | VernacTime [_,e] -> find true fail e + | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e | VernacFail e -> find time true e | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in Hooks.call Hooks.with_fail fail (fun () -> diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 180f20ae81..9edc1f1c70 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -490,6 +490,9 @@ let rec tmpp v loc = | VernacTime l -> xmlApply loc (Element("time",[],[]) :: List.map (fun(loc,e) ->tmpp e loc) l) + | VernacRedirect (s, l) -> + xmlApply loc (Element("redirect",["path", s],[]) :: + List.map (fun(loc,e) ->tmpp e loc) l) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 783ff2e116..2b5eb86834 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -86,7 +86,7 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e -> classify_vernac_list e + | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ |