# HG changeset patch
# User wenzelm
# Date 1354706575 -3600
# Node ID 2f8dc9e65401b7c27125faaa6739141d3d754ca1
# Parent  1a539d7a043845ea4df73a9612512c532ce8e22e
tuned signature in accordance to document operations;

diff -r 1a539d7a0438 -r 2f8dc9e65401 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Pure/System/session.scala	Wed Dec 05 12:22:55 2012 +0100
@@ -465,14 +465,6 @@
 
   def cancel_execution() { session_actor ! Cancel_Execution }
 
-  def edit(edits: List[Document.Edit_Text])
+  def update(edits: List[Document.Edit_Text])
   { session_actor !? Session.Raw_Edits(edits) }
-
-  def edit_node(name: Document.Node.Name,
-    header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
-  {
-    edit(List(header_edit(name, header),
-      name -> Document.Node.Edits(text_edits),
-      name -> Document.Node.Perspective(perspective)))
-  }
 }
diff -r 1a539d7a0438 -r 2f8dc9e65401 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Dec 05 12:22:55 2012 +0100
@@ -79,8 +79,6 @@
 
   /* perspective */
 
-  def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
-
   def node_perspective(): Text.Perspective =
   {
     Swing_Thread.require()
@@ -92,7 +90,7 @@
   }
 
 
-  /* initial edits */
+  /* edits */
 
   def init_edits(): List[Document.Edit_Text] =
   {
@@ -107,6 +105,17 @@
       name -> Document.Node.Perspective(perspective))
   }
 
+  def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit])
+    : List[Document.Edit_Text] =
+  {
+    Swing_Thread.require()
+    val header = node_header()
+
+    List(session.header_edit(name, header),
+      name -> Document.Node.Edits(text_edits),
+      name -> Document.Node.Perspective(perspective))
+  }
+
 
   /* pending edits */
 
@@ -126,7 +135,7 @@
       if (!edits.isEmpty || last_perspective != new_perspective) {
         pending.clear
         last_perspective = new_perspective
-        session.edit_node(name, node_header(), new_perspective, edits)
+        session.update(node_edits(new_perspective, edits))
       }
     }
 
@@ -148,7 +157,7 @@
     def init()
     {
       flush()
-      session.edit(init_edits())
+      session.update(init_edits())
     }
 
     def exit()
@@ -167,7 +176,7 @@
   def full_perspective()
   {
     pending_edits.flush()
-    session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
+    session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
   }
 
 
diff -r 1a539d7a0438 -r 2f8dc9e65401 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Dec 05 12:22:55 2012 +0100
@@ -79,7 +79,7 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    val buffer_range = model.buffer_range()
+    val buffer_range = JEdit_Lib.buffer_range(model.buffer)
     Text.Perspective(
       for {
         i <- 0 until text_area.getVisibleLines
diff -r 1a539d7a0438 -r 2f8dc9e65401 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Dec 05 12:22:55 2012 +0100
@@ -112,6 +112,12 @@
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
 
+  /* buffer range */
+
+  def buffer_range(buffer: JEditBuffer): Text.Range =
+    Text.Range(0, (buffer.getLength - 1) max 0)
+
+
   /* point range */
 
   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
diff -r 1a539d7a0438 -r 2f8dc9e65401 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Dec 05 12:22:55 2012 +0100
@@ -95,7 +95,7 @@
             model_edits ::: edits
           }
         }
-      PIDE.session.edit(init_edits)
+      PIDE.session.update(init_edits)
     }
   }