tuned signature;

--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -46,11 +46,11 @@
     }
   }
 
-  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
+  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
   {
     Swing_Thread.require()
     apply(buffer).map(_.deactivate)
-    val model = new Document_Model(session, buffer, name)
+    val model = new Document_Model(session, buffer, node_name)
     buffer.setProperty(key, model)
     model.activate()
     buffer.propertiesChanged
@@ -59,7 +59,7 @@
 }
 
 
-class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
+class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
 {
   /* header */
 
@@ -68,7 +68,7 @@
     Swing_Thread.require()
     JEdit_Lib.buffer_lock(buffer) {
       Exn.capture {
-        PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
+        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
       } match {
         case Exn.Res(header) => header
         case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
@@ -131,10 +131,10 @@
     val text = JEdit_Lib.buffer_text(buffer)
     val perspective = node_perspective()
 
-    List(session.header_edit(name, header),
-      name -> Document.Node.Clear(),
-      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
-      name -> perspective)
+    List(session.header_edit(node_name, header),
+      node_name -> Document.Node.Clear(),
+      node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+      node_name -> perspective)
   }
 
   def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
@@ -144,9 +144,9 @@
 
     val header = node_header()
 
-    List(session.header_edit(name, header),
-      name -> Document.Node.Edits(text_edits),
-      name -> perspective)
+    List(session.header_edit(node_name, header),
+      node_name -> Document.Node.Edits(text_edits),
+      node_name -> perspective)
   }
 
 
@@ -208,7 +208,7 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    session.snapshot(name, pending_edits.snapshot())
+    session.snapshot(node_name, pending_edits.snapshot())
   }
 
 

--- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -197,7 +197,7 @@
                 val snapshot = model.snapshot()
 
                 if (changed.assignment ||
-                    (changed.nodes.contains(model.name) &&
+                    (changed.nodes.contains(model.node_name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
                   Swing_Thread.later { overview.delay_repaint.invoke() }
 

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -21,7 +21,7 @@
     Swing_Thread.require { jEdit.getActiveView() }
 
   def current_node(view: View): Option[Document.Node.Name] =
-    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.name) }
+    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
 
   def current_snapshot(view: View): Option[Document.Snapshot] =
     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
@@ -35,7 +35,7 @@
       val text_area = view.getTextArea
       PIDE.document_view(text_area) match {
         case Some(doc_view) =>
-          val node = snapshot.version.nodes(doc_view.model.name)
+          val node = snapshot.version.nodes(doc_view.model.node_name)
           node.command_at(text_area.getCaretPosition)
         case None => None
       }

--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -97,7 +97,7 @@
               thy_load.buffer_node_name(buffer) match {
                 case Some(node_name) =>
                   document_model(buffer) match {
-                    case Some(model) if model.name == node_name => (Nil, Some(model))
+                    case Some(model) if model.node_name == node_name => (Nil, Some(model))
                     case _ =>
                       val model = Document_Model.init(session, buffer, node_name)
                       (model.init_edits(), Some(model))
@@ -175,7 +175,7 @@
 
         val thys =
           for (buffer <- buffers; model <- PIDE.document_model(buffer))
-            yield model.name
+            yield model.node_name
 
         val thy_info = new Thy_Info(PIDE.thy_load)
         // FIXME avoid I/O in Swing thread!?!

--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -98,7 +98,7 @@
       buffer <- JEdit_Lib.jedit_buffers
       model <- PIDE.document_model(buffer)
       if model.node_required
-    } nodes_required += model.name
+    } nodes_required += model.node_name
   }
   update_nodes_required()
 

--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 11:49:58 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 11:56:12 2013 +0200
@@ -165,7 +165,7 @@
     val name =
       Document_View(view.getTextArea) match {
         case None => Document.Node.Name.empty
-        case Some(doc_view) => doc_view.model.name
+        case Some(doc_view) => doc_view.model.node_name
       }
     val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)