tuned signature in accordance to document operations;
authorwenzelm
Wed Dec 05 12:22:55 2012 +0100 (2012-12-05)
changeset 503632f8dc9e65401
parent 50362 1a539d7a0438
child 50364 ce2796981c0c
tuned signature in accordance to document operations;
src/Pure/System/session.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/System/session.scala	Wed Dec 05 11:34:04 2012 +0100
     1.2 +++ b/src/Pure/System/session.scala	Wed Dec 05 12:22:55 2012 +0100
     1.3 @@ -465,14 +465,6 @@
     1.4  
     1.5    def cancel_execution() { session_actor ! Cancel_Execution }
     1.6  
     1.7 -  def edit(edits: List[Document.Edit_Text])
     1.8 +  def update(edits: List[Document.Edit_Text])
     1.9    { session_actor !? Session.Raw_Edits(edits) }
    1.10 -
    1.11 -  def edit_node(name: Document.Node.Name,
    1.12 -    header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
    1.13 -  {
    1.14 -    edit(List(header_edit(name, header),
    1.15 -      name -> Document.Node.Edits(text_edits),
    1.16 -      name -> Document.Node.Perspective(perspective)))
    1.17 -  }
    1.18  }
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Dec 05 11:34:04 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Dec 05 12:22:55 2012 +0100
     2.3 @@ -79,8 +79,6 @@
     2.4  
     2.5    /* perspective */
     2.6  
     2.7 -  def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
     2.8 -
     2.9    def node_perspective(): Text.Perspective =
    2.10    {
    2.11      Swing_Thread.require()
    2.12 @@ -92,7 +90,7 @@
    2.13    }
    2.14  
    2.15  
    2.16 -  /* initial edits */
    2.17 +  /* edits */
    2.18  
    2.19    def init_edits(): List[Document.Edit_Text] =
    2.20    {
    2.21 @@ -107,6 +105,17 @@
    2.22        name -> Document.Node.Perspective(perspective))
    2.23    }
    2.24  
    2.25 +  def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit])
    2.26 +    : List[Document.Edit_Text] =
    2.27 +  {
    2.28 +    Swing_Thread.require()
    2.29 +    val header = node_header()
    2.30 +
    2.31 +    List(session.header_edit(name, header),
    2.32 +      name -> Document.Node.Edits(text_edits),
    2.33 +      name -> Document.Node.Perspective(perspective))
    2.34 +  }
    2.35 +
    2.36  
    2.37    /* pending edits */
    2.38  
    2.39 @@ -126,7 +135,7 @@
    2.40        if (!edits.isEmpty || last_perspective != new_perspective) {
    2.41          pending.clear
    2.42          last_perspective = new_perspective
    2.43 -        session.edit_node(name, node_header(), new_perspective, edits)
    2.44 +        session.update(node_edits(new_perspective, edits))
    2.45        }
    2.46      }
    2.47  
    2.48 @@ -148,7 +157,7 @@
    2.49      def init()
    2.50      {
    2.51        flush()
    2.52 -      session.edit(init_edits())
    2.53 +      session.update(init_edits())
    2.54      }
    2.55  
    2.56      def exit()
    2.57 @@ -167,7 +176,7 @@
    2.58    def full_perspective()
    2.59    {
    2.60      pending_edits.flush()
    2.61 -    session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
    2.62 +    session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
    2.63    }
    2.64  
    2.65  
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Dec 05 11:34:04 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Dec 05 12:22:55 2012 +0100
     3.3 @@ -79,7 +79,7 @@
     3.4    def perspective(): Text.Perspective =
     3.5    {
     3.6      Swing_Thread.require()
     3.7 -    val buffer_range = model.buffer_range()
     3.8 +    val buffer_range = JEdit_Lib.buffer_range(model.buffer)
     3.9      Text.Perspective(
    3.10        for {
    3.11          i <- 0 until text_area.getVisibleLines
     4.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 05 11:34:04 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 05 12:22:55 2012 +0100
     4.3 @@ -112,6 +112,12 @@
     4.4      catch { case _: ArrayIndexOutOfBoundsException => None }
     4.5  
     4.6  
     4.7 +  /* buffer range */
     4.8 +
     4.9 +  def buffer_range(buffer: JEditBuffer): Text.Range =
    4.10 +    Text.Range(0, (buffer.getLength - 1) max 0)
    4.11 +
    4.12 +
    4.13    /* point range */
    4.14  
    4.15    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Dec 05 11:34:04 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Dec 05 12:22:55 2012 +0100
     5.3 @@ -95,7 +95,7 @@
     5.4              model_edits ::: edits
     5.5            }
     5.6          }
     5.7 -      PIDE.session.edit(init_edits)
     5.8 +      PIDE.session.update(init_edits)
     5.9      }
    5.10    }
    5.11