# HG changeset patch # User wenzelm # Date 1473850300 -7200 # Node ID 630eaf8fe9f3cda4f535be4ee922d93b7324a1ec # Parent ccac33e291b1243fba3bee865f4beb004915c65f tuned; diff -r ccac33e291b1 -r 630eaf8fe9f3 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Sep 14 12:12:44 2016 +0200 +++ b/src/Pure/General/path.scala Wed Sep 14 12:51:40 2016 +0200 @@ -96,7 +96,7 @@ else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) - new Path(norm_elems(elems.reverse ::: roots)) + new Path(norm_elems(elems reverse_::: roots)) } def is_wellformed(str: String): Boolean = diff -r ccac33e291b1 -r 630eaf8fe9f3 src/Pure/Thy/thy_syntax.scala --- 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))) }