diff options
| -rw-r--r-- | intf/vernacexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | toplevel/stm.ml | 23 | ||||
| -rw-r--r-- | toplevel/vernac_classifier.ml | 3 |
5 files changed, 20 insertions, 10 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 28c8c6c9f..d05a25596 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -219,6 +219,7 @@ type bullet = type 'a stm_vernac = | JoinDocument | Finish + | PrintDag | Observe of Stateid.t | Command of 'a (* An out of flow command not to be recorded by Stm *) | PGLast of 'a (* To ease the life of PG *) @@ -436,6 +437,7 @@ and vernac_part_of_script = bool and vernac_control = | VtFinish | VtJoinDocument + | VtPrintDag | VtObserve of Stateid.t | VtBack of Stateid.t type vernac_when = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index fe8e0787c..a00783a3b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -80,6 +80,7 @@ GEXTEND Gram (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish + | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> VernacStm (Observe (Stateid.of_int (int_of_string id))) | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 06d095818..bb0f4982b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -478,6 +478,7 @@ let rec pr_vernac = function (* Stm *) | VernacStm JoinDocument -> str"Stm JoinDocument" + | VernacStm PrintDag -> str"Stm PrintDag" | VernacStm Finish -> str"Stm Finish" | VernacStm (Observe id) -> str"Stm Observe " ++ str(Stateid.to_string id) diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 3be8318ac..478d69965 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -212,7 +212,7 @@ module VCS : sig val visit : id -> visit - val print : unit -> unit + val print : ?now:bool -> unit -> unit val backup : unit -> vcs val restore : vcs -> unit @@ -426,7 +426,7 @@ end = struct (* {{{ *) module NB : sig (* Non blocking Sys.command *) - val command : (unit -> unit) -> unit + val command : now:bool -> (unit -> unit) -> unit end = struct (* {{{ *) @@ -452,15 +452,18 @@ end = struct (* {{{ *) try while true do get_last_job () () done with e -> () (* No failure *) - let command job = (* job () *) - set_last_job job; - if Option.is_empty !worker then - worker := Some (Thread.create run_command ()) + let command ~now job = + if now then job () + else begin + set_last_job job; + if Option.is_empty !worker then + worker := Some (Thread.create run_command ()) + end end (* }}} *) - let print () = - if not !Flags.debug then () else NB.command (print_dag !vcs) + let print ?(now=false) () = + if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -1307,8 +1310,10 @@ let process_transaction ~tty verbose c (loc, expr) = (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok + | VtStm (VtPrintDag, b), VtNow -> + warn_if_pos x b; VCS.print ~now:true (); `Ok | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument), _), VtLater -> + | VtStm ((VtObserve _ | VtFinish | VtJoinDocument|VtPrintDag),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") (* Back *) diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index f773856ff..2edd2fa2d 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -21,7 +21,7 @@ let string_of_vernac_type = function | VtProofStep -> "ProofStep" | VtProofMode s -> "ProofMode " ^ s | VtQuery b -> "Query" ^ string_of_in_script b - | VtStm ((VtFinish|VtJoinDocument|VtObserve _), b) -> + | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag), b) -> "Stm" ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b @@ -53,6 +53,7 @@ let rec classify_vernac e = (* Stm *) | VernacStm Finish -> VtStm (VtFinish, true), VtNow | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow + | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow |