--- a/src/Pure/PIDE/document.scala Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sun Aug 15 21:42:13 2010 +0200
@@ -34,7 +34,7 @@
/* named nodes -- development graph */
- type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove
+ type Node_Text_Edit = (String, List[Text.Edit]) // FIXME None: remove
type Edit[C] =
(String, // node name
@@ -141,7 +141,7 @@
def tip: Change = undo_list.head
def +(ch: Change): History = new History(ch :: undo_list)
- def snapshot(name: String, pending_edits: List[Text_Edit], state_snapshot: State): Snapshot =
+ def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
{
val found_stable = undo_list.find(change =>
change.is_finished && state_snapshot.is_assigned(change.current.join))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/text.scala Sun Aug 15 21:42:13 2010 +0200
@@ -0,0 +1,61 @@
+/* Title: Pure/PIDE/text.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+Basic operations on plain text.
+*/
+
+package isabelle
+
+
+object Text
+{
+ /* edits */
+
+ object Edit
+ {
+ def insert(start: Int, text: String): Edit = new Edit(true, start, text)
+ def remove(start: Int, text: String): Edit = new Edit(false, start, text)
+ }
+
+ class Edit(val is_insert: Boolean, val start: Int, val text: String)
+ {
+ override def toString =
+ (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
+
+
+ /* transform offsets */
+
+ private def transform(do_insert: Boolean, offset: Int): Int =
+ if (offset < start) offset
+ else if (is_insert == do_insert) offset + text.length
+ else (offset - text.length) max start
+
+ def convert(offset: Int): Int = transform(true, offset)
+ def revert(offset: Int): Int = transform(false, offset)
+
+
+ /* edit strings */
+
+ private def insert(index: Int, string: String): String =
+ string.substring(0, index) + text + string.substring(index)
+
+ private def remove(index: Int, count: Int, string: String): String =
+ string.substring(0, index) + string.substring(index + count)
+
+ def can_edit(string: String, shift: Int): Boolean =
+ shift <= start && start < shift + string.length
+
+ def edit(string: String, shift: Int): (Option[Edit], String) =
+ if (!can_edit(string, shift)) (Some(this), string)
+ else if (is_insert) (None, insert(start - shift, string))
+ else {
+ val index = start - shift
+ val count = text.length min (string.length - index)
+ val rest =
+ if (count == text.length) None
+ else Some(Edit.remove(start, text.substring(count)))
+ (rest, remove(index, count, string))
+ }
+ }
+}
--- a/src/Pure/PIDE/text_edit.scala Sun Aug 15 21:03:13 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-/* Title: Pure/PIDE/text_edit.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Basic edits on plain text.
-*/
-
-package isabelle
-
-
-class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
-{
- override def toString =
- (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
-
-
- /* transform offsets */
-
- private def transform(do_insert: Boolean, offset: Int): Int =
- if (offset < start) offset
- else if (is_insert == do_insert) offset + text.length
- else (offset - text.length) max start
-
- def convert(offset: Int): Int = transform(true, offset)
- def revert(offset: Int): Int = transform(false, offset)
-
-
- /* edit strings */
-
- private def insert(index: Int, string: String): String =
- string.substring(0, index) + text + string.substring(index)
-
- private def remove(index: Int, count: Int, string: String): String =
- string.substring(0, index) + string.substring(index + count)
-
- def can_edit(string: String, shift: Int): Boolean =
- shift <= start && start < shift + string.length
-
- def edit(string: String, shift: Int): (Option[Text_Edit], String) =
- if (!can_edit(string, shift)) (Some(this), string)
- else if (is_insert) (None, insert(start - shift, string))
- else {
- val index = start - shift
- val count = text.length min (string.length - index)
- val rest =
- if (count == text.length) None
- else Some(new Text_Edit(false, start, text.substring(count)))
- (rest, remove(index, count, string))
- }
-}
-
--- a/src/Pure/System/session.scala Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Pure/System/session.scala Sun Aug 15 21:42:13 2010 +0200
@@ -292,7 +292,7 @@
{
@volatile private var history = Document.History.init
- def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
history.snapshot(name, pending_edits, current_state())
def act
@@ -328,7 +328,7 @@
def stop() { session_actor ! Stop }
- def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
editor_history.snapshot(name, pending_edits)
def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
--- a/src/Pure/Thy/thy_syntax.scala Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sun Aug 15 21:42:13 2010 +0200
@@ -43,7 +43,7 @@
{
/* phase 1: edit individual command source */
- @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command])
+ @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
: Linear_Set[Command] =
{
eds match {
--- a/src/Pure/build-jars Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Pure/build-jars Sun Aug 15 21:42:13 2010 +0200
@@ -41,7 +41,7 @@
PIDE/document.scala
PIDE/event_bus.scala
PIDE/markup_node.scala
- PIDE/text_edit.scala
+ PIDE/text.scala
System/cygwin.scala
System/download.scala
System/gui_setup.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Aug 15 21:42:13 2010 +0200
@@ -199,14 +199,14 @@
object pending_edits // owned by Swing thread
{
- private val pending = new mutable.ListBuffer[Text_Edit]
- def snapshot(): List[Text_Edit] = pending.toList
+ private val pending = new mutable.ListBuffer[Text.Edit]
+ def snapshot(): List[Text.Edit] = pending.toList
private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
}
- def flush(): List[Text_Edit] =
+ def flush(): List[Text.Edit] =
{
Swing_Thread.require()
val edits = snapshot()
@@ -214,7 +214,7 @@
edits
}
- def +=(edit: Text_Edit)
+ def +=(edit: Text.Edit)
{
Swing_Thread.require()
pending += edit
@@ -239,13 +239,13 @@
override def contentInserted(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, length: Int)
{
- pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
+ pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
}
override def preContentRemoved(buffer: JEditBuffer,
start_line: Int, start: Int, num_lines: Int, removed_length: Int)
{
- pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
+ pending_edits += Text.Edit.remove(start, buffer.getText(start, removed_length))
}
}
@@ -321,7 +321,7 @@
buffer.setTokenMarker(token_marker)
buffer.addBufferListener(buffer_listener)
buffer.propertiesChanged()
- pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
+ pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
}
def refresh()