| changeset 63866 | 630eaf8fe9f3 |
| parent 63584 | 68751fe1c036 |
| child 64799 | c0c648911f1a |
--- a/src/Pure/Thy/thy_syntax.scala Wed Sep 14 12:12:44 2016 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Sep 14 12:51:40 2016 +0200 @@ -198,7 +198,7 @@ val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList - removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) ::: + removed.map(cmd => (old_cmds.prev(cmd), None)) reverse_::: inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd))) }