Basic edits on plain text.

--- a/src/Pure/IsaMakefile	Tue Jan 05 16:55:00 2010 +0100
+++ b/src/Pure/IsaMakefile	Tue Jan 05 18:20:18 2010 +0100
@@ -131,8 +131,8 @@
   System/isabelle_process.scala System/isabelle_syntax.scala		\
   System/isabelle_system.scala System/platform.scala			\
   System/session_manager.scala System/standard_system.scala		\
-  Thy/completion.scala Thy/html.scala Thy/thy_header.scala		\
-  Thy/thy_syntax.scala library.scala
+  Thy/completion.scala Thy/html.scala Thy/text_edit.scala		\
+  Thy/thy_header.scala Thy/thy_syntax.scala library.scala
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes
 PURE_JAR = $(JAR_DIR)/Pure.jar

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/text_edit.scala	Tue Jan 05 18:20:18 2010 +0100
@@ -0,0 +1,43 @@
+/*  Title:      Pure/Thy/text_edit.scala
+    Author:     Fabian Immler, TU Munich
+    Author:     Makarius
+
+Basic edits on plain text.
+*/
+
+package isabelle
+
+
+sealed abstract class Text_Edit
+{
+  val start: Int
+  def before(offset: Int): Int
+  def after(offset: Int): Int
+}
+
+
+object Text_Edit
+{
+  case class Insert(start: Int, text: String) extends Text_Edit
+  {
+    def before(offset: Int): Int =
+      if (start > offset) offset
+      else (offset - text.length) max start
+
+    def after(offset: Int): Int =
+      if (start <= offset) offset + text.length
+      else offset
+  }
+
+  case class Remove(start: Int, text: String) extends Text_Edit
+  {
+    def before(offset: Int): Int =
+      if (start <= offset) offset + text.length
+      else offset
+
+    def after(offset: Int): Int =
+      if (start > offset) offset
+      else (offset - text.length) max start
+  }
+}
+