diff options
| author | Enrico Tassi | 2014-10-22 15:12:51 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-22 16:00:01 +0200 |
| commit | ad28bacca8cf9f779db099f7c42938b96ae31f42 (patch) | |
| tree | f0cceec16fc36bfa586bad7b0a0536215527ce5d /lib | |
| parent | 356597ffc42b9298e27e0af2cfd05fe73f6d1383 (diff) | |
Goal printing made uniform: always done in STM (close 3585)
Goal printing was partially broken. Some commands in vernacentries
were printing, but not all of them. Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.
Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs. More modern GUI do ask for the goals.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index a744ce9b0b..d94482cebf 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -8,7 +8,7 @@ let with_option o f x = let old = !o in o:=true; - try let r = f x in o := old; r + try let r = f x in if !o = true then o := old; r with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = o := old in @@ -27,7 +27,7 @@ let with_options ol f x = let without_option o f x = let old = !o in o:=false; - try let r = f x in o := old; r + try let r = f x in if !o = false then o := old; r with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = o := old in |