changeset 54513 | 5545aff878b1 |
parent 54511 | 1fd24c96ce9b |
child 54521 | 744ea0025e11 |
--- a/src/Tools/jEdit/src/document_model.scala Mon Nov 18 22:06:08 2013 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 18 23:26:15 2013 +0100 @@ -190,7 +190,7 @@ val clear = pending_clear val edits = snapshot() val perspective = node_perspective() - if (clear || !edits.isEmpty || last_perspective != perspective) { + if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) { pending_clear = false pending.clear last_perspective = perspective