diff options
| author | Hugo Herbelin | 2016-04-27 22:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:04 +0200 |
| commit | ee46e2744d68dd7402d38cfbc63d1d523fce9cdc (patch) | |
| tree | aa3c05f348b7520ccfe407db1301788a55f58673 | |
| parent | 141296307ad81fd1f6d69c0827fd284a81587abc (diff) | |
Revert "Protect the beautifier from change in the lexer state (typically by"
This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d92f02ddd6..89bc31d0ac 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -229,9 +229,7 @@ let rec vernac_com verbose checknav (loc,com) = if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in - let a = Lexer.com_state () in - interp com; - Lexer.restore_com_state a + interp com with reraise -> let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; |
