moved Text_Edit to Text.Edit;
authorwenzelm
Sun Aug 15 21:42:13 2010 +0200 (2010-08-15)
changeset 38425e467db701d78
parent 38424 940a404e45e2
child 38426 2858ec7b6dd8
moved Text_Edit to Text.Edit;
tuned;
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/text_edit.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 15 21:03:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 15 21:42:13 2010 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5    /* named nodes -- development graph */
     1.6  
     1.7 -  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
     1.8 +  type Node_Text_Edit = (String, List[Text.Edit])  // FIXME None: remove
     1.9  
    1.10    type Edit[C] =
    1.11     (String,  // node name
    1.12 @@ -141,7 +141,7 @@
    1.13      def tip: Change = undo_list.head
    1.14      def +(ch: Change): History = new History(ch :: undo_list)
    1.15  
    1.16 -    def snapshot(name: String, pending_edits: List[Text_Edit], state_snapshot: State): Snapshot =
    1.17 +    def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
    1.18      {
    1.19        val found_stable = undo_list.find(change =>
    1.20          change.is_finished && state_snapshot.is_assigned(change.current.join))
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 15 21:42:13 2010 +0200
     2.3 @@ -0,0 +1,61 @@
     2.4 +/*  Title:      Pure/PIDE/text.scala
     2.5 +    Author:     Fabian Immler, TU Munich
     2.6 +    Author:     Makarius
     2.7 +
     2.8 +Basic operations on plain text.
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +object Text
    2.15 +{
    2.16 +  /* edits */
    2.17 +
    2.18 +  object Edit
    2.19 +  {
    2.20 +    def insert(start: Int, text: String): Edit = new Edit(true, start, text)
    2.21 +    def remove(start: Int, text: String): Edit = new Edit(false, start, text)
    2.22 +  }
    2.23 +
    2.24 +  class Edit(val is_insert: Boolean, val start: Int, val text: String)
    2.25 +  {
    2.26 +    override def toString =
    2.27 +      (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    2.28 +
    2.29 +
    2.30 +    /* transform offsets */
    2.31 +
    2.32 +    private def transform(do_insert: Boolean, offset: Int): Int =
    2.33 +      if (offset < start) offset
    2.34 +      else if (is_insert == do_insert) offset + text.length
    2.35 +      else (offset - text.length) max start
    2.36 +
    2.37 +    def convert(offset: Int): Int = transform(true, offset)
    2.38 +    def revert(offset: Int): Int = transform(false, offset)
    2.39 +
    2.40 +
    2.41 +    /* edit strings */
    2.42 +
    2.43 +    private def insert(index: Int, string: String): String =
    2.44 +      string.substring(0, index) + text + string.substring(index)
    2.45 +
    2.46 +    private def remove(index: Int, count: Int, string: String): String =
    2.47 +      string.substring(0, index) + string.substring(index + count)
    2.48 +
    2.49 +    def can_edit(string: String, shift: Int): Boolean =
    2.50 +      shift <= start && start < shift + string.length
    2.51 +
    2.52 +    def edit(string: String, shift: Int): (Option[Edit], String) =
    2.53 +      if (!can_edit(string, shift)) (Some(this), string)
    2.54 +      else if (is_insert) (None, insert(start - shift, string))
    2.55 +      else {
    2.56 +        val index = start - shift
    2.57 +        val count = text.length min (string.length - index)
    2.58 +        val rest =
    2.59 +          if (count == text.length) None
    2.60 +          else Some(Edit.remove(start, text.substring(count)))
    2.61 +        (rest, remove(index, count, string))
    2.62 +      }
    2.63 +  }
    2.64 +}
     3.1 --- a/src/Pure/PIDE/text_edit.scala	Sun Aug 15 21:03:13 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,51 +0,0 @@
     3.4 -/*  Title:      Pure/PIDE/text_edit.scala
     3.5 -    Author:     Fabian Immler, TU Munich
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Basic edits on plain text.
     3.9 -*/
    3.10 -
    3.11 -package isabelle
    3.12 -
    3.13 -
    3.14 -class Text_Edit(val is_insert: Boolean, val start: Int, val text: String)
    3.15 -{
    3.16 -  override def toString =
    3.17 -    (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    3.18 -
    3.19 -
    3.20 -  /* transform offsets */
    3.21 -
    3.22 -  private def transform(do_insert: Boolean, offset: Int): Int =
    3.23 -    if (offset < start) offset
    3.24 -    else if (is_insert == do_insert) offset + text.length
    3.25 -    else (offset - text.length) max start
    3.26 -
    3.27 -  def convert(offset: Int): Int = transform(true, offset)
    3.28 -  def revert(offset: Int): Int = transform(false, offset)
    3.29 -
    3.30 -
    3.31 -  /* edit strings */
    3.32 -
    3.33 -  private def insert(index: Int, string: String): String =
    3.34 -    string.substring(0, index) + text + string.substring(index)
    3.35 -
    3.36 -  private def remove(index: Int, count: Int, string: String): String =
    3.37 -    string.substring(0, index) + string.substring(index + count)
    3.38 -
    3.39 -  def can_edit(string: String, shift: Int): Boolean =
    3.40 -    shift <= start && start < shift + string.length
    3.41 -
    3.42 -  def edit(string: String, shift: Int): (Option[Text_Edit], String) =
    3.43 -    if (!can_edit(string, shift)) (Some(this), string)
    3.44 -    else if (is_insert) (None, insert(start - shift, string))
    3.45 -    else {
    3.46 -      val index = start - shift
    3.47 -      val count = text.length min (string.length - index)
    3.48 -      val rest =
    3.49 -        if (count == text.length) None
    3.50 -        else Some(new Text_Edit(false, start, text.substring(count)))
    3.51 -      (rest, remove(index, count, string))
    3.52 -    }
    3.53 -}
    3.54 -
     4.1 --- a/src/Pure/System/session.scala	Sun Aug 15 21:03:13 2010 +0200
     4.2 +++ b/src/Pure/System/session.scala	Sun Aug 15 21:42:13 2010 +0200
     4.3 @@ -292,7 +292,7 @@
     4.4    {
     4.5      @volatile private var history = Document.History.init
     4.6  
     4.7 -    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
     4.8 +    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     4.9        history.snapshot(name, pending_edits, current_state())
    4.10  
    4.11      def act
    4.12 @@ -328,7 +328,7 @@
    4.13  
    4.14    def stop() { session_actor ! Stop }
    4.15  
    4.16 -  def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
    4.17 +  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    4.18      editor_history.snapshot(name, pending_edits)
    4.19  
    4.20    def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 21:03:13 2010 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 21:42:13 2010 +0200
     5.3 @@ -43,7 +43,7 @@
     5.4    {
     5.5      /* phase 1: edit individual command source */
     5.6  
     5.7 -    @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command])
     5.8 +    @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
     5.9          : Linear_Set[Command] =
    5.10      {
    5.11        eds match {
     6.1 --- a/src/Pure/build-jars	Sun Aug 15 21:03:13 2010 +0200
     6.2 +++ b/src/Pure/build-jars	Sun Aug 15 21:42:13 2010 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4    PIDE/document.scala
     6.5    PIDE/event_bus.scala
     6.6    PIDE/markup_node.scala
     6.7 -  PIDE/text_edit.scala
     6.8 +  PIDE/text.scala
     6.9    System/cygwin.scala
    6.10    System/download.scala
    6.11    System/gui_setup.scala
     7.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 21:03:13 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 21:42:13 2010 +0200
     7.3 @@ -199,14 +199,14 @@
     7.4  
     7.5    object pending_edits  // owned by Swing thread
     7.6    {
     7.7 -    private val pending = new mutable.ListBuffer[Text_Edit]
     7.8 -    def snapshot(): List[Text_Edit] = pending.toList
     7.9 +    private val pending = new mutable.ListBuffer[Text.Edit]
    7.10 +    def snapshot(): List[Text.Edit] = pending.toList
    7.11  
    7.12      private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
    7.13        if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
    7.14      }
    7.15  
    7.16 -    def flush(): List[Text_Edit] =
    7.17 +    def flush(): List[Text.Edit] =
    7.18      {
    7.19        Swing_Thread.require()
    7.20        val edits = snapshot()
    7.21 @@ -214,7 +214,7 @@
    7.22        edits
    7.23      }
    7.24  
    7.25 -    def +=(edit: Text_Edit)
    7.26 +    def +=(edit: Text.Edit)
    7.27      {
    7.28        Swing_Thread.require()
    7.29        pending += edit
    7.30 @@ -239,13 +239,13 @@
    7.31      override def contentInserted(buffer: JEditBuffer,
    7.32        start_line: Int, offset: Int, num_lines: Int, length: Int)
    7.33      {
    7.34 -      pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
    7.35 +      pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
    7.36      }
    7.37  
    7.38      override def preContentRemoved(buffer: JEditBuffer,
    7.39        start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    7.40      {
    7.41 -      pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
    7.42 +      pending_edits += Text.Edit.remove(start, buffer.getText(start, removed_length))
    7.43      }
    7.44    }
    7.45  
    7.46 @@ -321,7 +321,7 @@
    7.47      buffer.setTokenMarker(token_marker)
    7.48      buffer.addBufferListener(buffer_listener)
    7.49      buffer.propertiesChanged()
    7.50 -    pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
    7.51 +    pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
    7.52    }
    7.53  
    7.54    def refresh()