diff options
| author | Emilio Jesus Gallego Arias | 2017-05-18 07:31:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-01 15:50:26 +0200 |
| commit | 6b041a242607ec906fbab451e53c15af6339e4ef (patch) | |
| tree | ac7b4e6a25c0607c1770da551ed4f5de4addb310 /stm/stm.ml | |
| parent | f3a388baf9cf2a14a658cab77554a0802b999486 (diff) | |
[emacs] [toplevel] Make emacs flag local to the toplevel.
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index b98cb312ed..2057496f4b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -66,7 +66,7 @@ end (* During interactive use we cache more states so that Undoing is fast *) let interactive () = - if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes + if !Flags.ide_slave || not !Flags.batch_mode then `Yes else `No let async_proofs_workers_extra_env = ref [||] @@ -1094,7 +1094,7 @@ end = struct (* {{{ *) VtStm (VtBack oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow + VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow | _ -> VtUnknown, VtNow with | Not_found -> |