diff options
| author | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /stm | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 3 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
3 files changed, 7 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 38745e2273..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 () -> @@ -2018,7 +2018,7 @@ let handle_failure (e, info) vcs tty = end; VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ - Errors.print_no_report e) + Errors.iprint_no_report (e, info)) | Some (safe_id, id) -> prerr_endline ("Failed at state " ^ Stateid.to_string id); VCS.restore vcs; 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 _ |