# HG changeset patch
# User wenzelm
# Date 1357584466 -3600
# Node ID 7d89bb992f48a22d9fffc4b51b6e5463d90405f9
# Parent  eee13361ec0a4a564459bf1ad6d0769e032cf885# Parent  f6811984983b3bb6f76346315b933c6684590ad0
merged

diff -r eee13361ec0a -r 7d89bb992f48 src/Pure/Thy/thy_syntax.scala
--- 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