changeset 73120 | c3589f2dff31 |
parent 71601 | 97ccf48c2f0c |
child 73340 | 0ffcad1f6130 |
--- a/src/Pure/Thy/thy_syntax.scala Sat Jan 09 22:41:08 2021 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sun Jan 10 13:04:29 2021 +0100 @@ -140,7 +140,7 @@ edit_text(es, insert_text(Some(cmd), e.text)) case None => - require(e.is_insert && e.start == 0) + require(e.is_insert && e.start == 0, "bad text edit") edit_text(es, insert_text(None, e.text)) } case Nil => commands