diff options
| author | gareuselesinge | 2013-11-05 16:02:44 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-11-05 16:02:44 +0000 |
| commit | ca940a5ed0fa202931949010dd0814c79a6b996d (patch) | |
| tree | 8b894d1858aef9937408bfd78f53fa45ecb52a08 | |
| parent | 6fea2f181221155535fdd86f67ae10077876ca6d (diff) | |
STM: fix for PG and "Proof term" lines.
PG sends "Set Silent" and it was messing up the DAG, making the
detection of an immediate proof not working.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17061 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
| -rw-r--r-- | toplevel/stm.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac_classifier.ml | 5 |
3 files changed, 9 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8bf65d0445..d1ed1d4abb 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -452,6 +452,7 @@ and vernac_control = | VtPrintDag | VtObserve of Stateid.t | VtBack of Stateid.t + | VtPG type vernac_when = | VtNow | VtLater diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 2411eed6ec..a5a40b0a73 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1412,6 +1412,9 @@ let process_transaction ~tty verbose c (loc, expr) = let rc = begin prerr_endline (" classified as: " ^ string_of_vernac_classification c); match c with + (* PG stuff *) + | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok + | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* 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 diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 139dc67d7a..2e04d14302 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -23,6 +23,7 @@ let string_of_vernac_type = function | VtQuery b -> "Query" ^ string_of_in_script b | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> "Stm" ^ string_of_in_script b + | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b let string_of_vernac_when = function @@ -50,6 +51,10 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with + (* PG compatibility *) + | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) + | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) + when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* Stm *) | VernacStm Finish -> VtStm (VtFinish, true), VtNow | VernacStm Wait -> VtStm (VtWait, true), VtNow |