# HG changeset patch
# User wenzelm
# Date 1357477875 -3600
# Node ID f6811984983b3bb6f76346315b933c6684590ad0
# Parent  1253fd12ca8a616a0d1f195e1509320d8f9d25f8
export some generally useful operations;

diff -r 1253fd12ca8a -r f6811984983b src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Jan 06 12:44:45 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Jan 06 14:11:15 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