--- a/src/Pure/Thy/thy_syntax.scala Mon Jan 07 11:59:37 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 07 19:47:46 2013 +0100
@@ -169,8 +169,7 @@
/* edit individual command source */
- @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
- : Linear_Set[Command] =
+ @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
{
eds match {
case e :: es =>
@@ -293,7 +292,7 @@
/* main */
- private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
+ def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
: List[(Option[Command], Option[Command])] =
{
val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList