# HG changeset patch # User wenzelm # Date 1281901333 -7200 # Node ID e467db701d781f39fba50e34445db410bde91b88 # Parent 940a404e45e274352040a7e0dbc68849711ee3ed moved Text_Edit to Text.Edit; tuned; diff -r 940a404e45e2 -r e467db701d78 src/Pure/PIDE/document.scala --- 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)) diff -r 940a404e45e2 -r e467db701d78 src/Pure/PIDE/text.scala --- /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)) + } + } +} diff -r 940a404e45e2 -r e467db701d78 src/Pure/PIDE/text_edit.scala --- 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)) - } -} - diff -r 940a404e45e2 -r e467db701d78 src/Pure/System/session.scala --- 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) } diff -r 940a404e45e2 -r e467db701d78 src/Pure/Thy/thy_syntax.scala --- 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 { diff -r 940a404e45e2 -r e467db701d78 src/Pure/build-jars --- 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 diff -r 940a404e45e2 -r e467db701d78 src/Tools/jEdit/src/jedit/document_model.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()