Lemma bar ...
Edited Tactic.
Search bla bla.
Lemma foo ...
the document state gets printed fine, but the calculation of the next sentence is off, in particular Edited Tactic and Search ... are "glued".
We should check which data structure (the id -> sentence map or the end_offset -> sentence map) is used to compute the next sentence, and if the bug is in the code updating the data structure or the code computing the next sentence. The first data structure seems correct when printed.
After an editing session
the document state gets printed fine, but the calculation of the next sentence is off, in particular
Edited Tactic
andSearch ...
are "glued".We should check which data structure (the
id -> sentence
map or theend_offset -> sentence
map) is used to compute the next sentence, and if the bug is in the code updating the data structure or the code computing the next sentence. The first data structure seems correct when printed.