diff options
| author | Maxime Dénès | 2017-05-20 01:25:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-20 01:25:13 +0200 |
| commit | a78bfb93a6ece86b1f56f41d12d900d369444451 (patch) | |
| tree | 806c5b4bdcd1e9388031f8f0836c00375a75398f | |
| parent | 545ec516b35e3a036e6c3db194da780457463535 (diff) | |
| parent | 6ef8a007e77c61d9f8c2b19b19dc22548f1896ca (diff) | |
Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8f50bfb3d8..41d370ea57 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -641,6 +641,9 @@ let init_toplevel arglist = init_library_roots (); load_vernac_obj (); require (); + (* XXX: This is incorrect in batch mode, as we will initialize + the STM before having done Declaremods.start_library, thus + state 1 is invalid. This bug was present in 8.5/8.6. *) Stm.init (); let sid = load_rcfile (Stm.get_current_state ()) in (* XXX: We ignore this for now, but should be threaded to the toplevels *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cf0e8e759f..deb2cc1e3f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -164,7 +164,9 @@ let rec interp_vernac sid (loc,com) = let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> - ignore(Stm.edit_at sid); + (* XXX: In non-interactive mode edit_at seems to do very weird + things, so we better avoid it while we investigate *) + if not !Flags.batch_mode then ignore(Stm.edit_at sid); let (reraise, info) = CErrors.push reraise in let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) |