export some generally useful operations;

--- 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