tuned signature;

--- a/src/Pure/Thy/text_edit.scala	Sun Jan 10 17:29:09 2010 +0100
+++ b/src/Pure/Thy/text_edit.scala	Sun Jan 10 23:16:18 2010 +0100
@@ -11,8 +11,10 @@
 sealed abstract class Text_Edit
 {
   val start: Int
+  def text: String
   def after(offset: Int): Int
   def before(offset: Int): Int
+  def can_edit(string_length: Int, shift: Int): Boolean
   def edit(string: String, shift: Int): (Option[Text_Edit], String)
 }