# HG changeset patch
# User wenzelm
# Date 1396898582 -7200
# Node ID eea4bbe157455dc1f0296435398790e5efc90d5d
# Parent  16d4213d4cbc9db20ab4187ddc10cb00647fe702
tuned signature -- prefer static type Document.Node.Name;

diff -r 16d4213d4cbc -r eea4bbe15745 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -119,7 +119,7 @@
         for {
           cmd <- snapshot.node.load_commands
           blob_name <- cmd.blobs_names
-          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
           start <- snapshot.node.command_start(cmd)
           range = snapshot.convert(cmd.proper_range + start)
diff -r 16d4213d4cbc -r eea4bbe15745 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -52,7 +52,7 @@
   {
     Swing_Thread.require()
 
-    JEdit_Lib.jedit_buffer(name.node) match {
+    JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
         PIDE.document_model(buffer) match {
           case Some(model) => model.snapshot
diff -r 16d4213d4cbc -r eea4bbe15745 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -120,6 +120,9 @@
   def jedit_buffer(name: String): Option[Buffer] =
     jedit_buffers().find(buffer => buffer_name(buffer) == name)
 
+  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
+    jedit_buffer(name.node)
+
   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
 
   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
diff -r 16d4213d4cbc -r eea4bbe15745 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -57,7 +57,7 @@
   override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   {
     Swing_Thread.now {
-      JEdit_Lib.jedit_buffer(name.node) match {
+      JEdit_Lib.jedit_buffer(name) match {
         case Some(buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
             Some(f(buffer.getSegment(0, buffer.getLength)))
diff -r 16d4213d4cbc -r eea4bbe15745 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 07 16:37:57 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 07 21:23:02 2014 +0200
@@ -41,7 +41,7 @@
           if (in_checkbox(peer.indexToLocation(index), point)) {
             if (clicks == 1) {
               for {
-                buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
+                buffer <- JEdit_Lib.jedit_buffer(listData(index))
                 model <- PIDE.document_model(buffer)
               } model.node_required = !model.node_required
             }