# HG changeset patch
# User wenzelm
# Date 1263161778 -3600
# Node ID 9bb71dfe7314551c4c9f7b5b344028db4a8815bd
# Parent  78c10aea025d95847b762698b418b9902485c3fd
tuned signature;

diff -r 78c10aea025d -r 9bb71dfe7314 src/Pure/Thy/text_edit.scala
--- 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)
 }