diff options
author | 2016-04-10 17:04:44 +0200 | |
---|---|---|
committer | 2016-06-16 17:30:17 +0200 | |
commit | a4ff40931201f91cde79c212a9d2cc19a62b8128 (patch) | |
tree | e741a660a342c935d2cc81ef7db7f39dafa920e7 /toplevel | |
parent | 53e8a445177501846c75147680da03a95d5e9b5c (diff) |
Protect the beautifier from change in the lexer state (typically by
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0a32c88d6..94972e272 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -228,7 +228,9 @@ 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 - interp com + let a = CLexer.com_state () in + interp com; + CLexer.restore_com_state a with reraise -> let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; |