# HG changeset patch
# User wenzelm
# Date 1484216225 -3600
# Node ID c3b42ac0cf813215f193245c500cc30837320b9a
# Parent  9eff4c62579a6c31f1aae217253150dbdf4e42fe
tuned signature;

diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/active.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -18,7 +18,7 @@
   {
     GUI_Thread.require {}
 
-    Document_View(view.getTextArea) match {
+    Document_View.get(view.getTextArea) match {
       case Some(doc_view) =>
         doc_view.rich_text_area.robust_body() {
           val text_area = doc_view.text_area
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -350,7 +350,7 @@
       }
 
       if (buffer.isEditable) {
-        val opt_rendering = PIDE.document_view(text_area).map(_.get_rendering())
+        val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
         val result0 = syntax_completion(history, explicit, opt_rendering)
         val (no_completion, semantic_completion) =
         {
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -42,7 +42,7 @@
   {
     GUI_Thread.require {}
 
-    PIDE.document_view(text_area) match {
+    Document_View.get(text_area) match {
       case Some(doc_view) =>
         val rendering = doc_view.get_rendering()
         val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -25,7 +25,7 @@
 
   private val key = new Object
 
-  def apply(text_area: TextArea): Option[Document_View] =
+  def get(text_area: TextArea): Option[Document_View] =
   {
     GUI_Thread.require {}
     text_area.getClientProperty(key) match {
@@ -37,7 +37,7 @@
   def exit(text_area: JEditTextArea)
   {
     GUI_Thread.require {}
-    apply(text_area) match {
+    get(text_area) match {
       case None =>
       case Some(doc_view) =>
         doc_view.deactivate()
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -353,7 +353,7 @@
   def select_entity(text_area: JEditTextArea)
   {
     for {
-      doc_view <- PIDE.document_view(text_area)
+      doc_view <- Document_View.get(text_area)
       rendering = doc_view.get_rendering()
     } {
       val caret_range = JEdit_Lib.caret_range(text_area)
@@ -416,7 +416,7 @@
   {
     for {
       spell_checker <- PIDE.spell_checker.get
-      doc_view <- PIDE.document_view(text_area)
+      doc_view <- Document_View.get(text_area)
       rendering = doc_view.get_rendering()
       range = JEdit_Lib.caret_range(text_area)
       Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -42,7 +42,7 @@
   def visible_node(name: Document.Node.Name): Boolean =
     (for {
       text_area <- JEdit_Lib.jedit_text_areas()
-      doc_view <- Document_View(text_area)
+      doc_view <- Document_View.get(text_area)
     } yield doc_view.model.node_name).contains(name)
 
 
@@ -73,7 +73,7 @@
     val text_area = view.getTextArea
     val buffer = view.getBuffer
 
-    PIDE.document_view(text_area) match {
+    Document_View.get(text_area) match {
       case Some(doc_view) if doc_view.model.is_theory =>
         val node = snapshot.version.nodes(doc_view.model.node_name)
         val caret = snapshot.revert(text_area.getCaretPosition)
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -68,12 +68,10 @@
 
   /* document model and view */
 
-  def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
-
   def document_views(buffer: Buffer): List[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
-      doc_view <- document_view(text_area)
+      doc_view <- Document_View.get(text_area)
     } yield doc_view
 
   def exit_models(buffers: List[Buffer])
@@ -102,7 +100,7 @@
             val model = Document_Model.init(session, node_name, buffer)
             for {
               text_area <- JEdit_Lib.jedit_text_areas(buffer)
-              if document_view(text_area).map(_.model) != Some(model)
+              if Document_View.get(text_area).map(_.model) != Some(model)
             } Document_View.init(model, text_area)
           }
         }
@@ -144,7 +142,7 @@
   def rendering(view: View): JEdit_Rendering = GUI_Thread.now
   {
     val text_area = view.getTextArea
-    document_view(text_area) match {
+    Document_View.get(text_area) match {
       case Some(doc_view) => doc_view.get_rendering()
       case None => error("No document view for current text area")
     }
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/spell_checker.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -100,7 +100,7 @@
     val result =
       for {
         spell_checker <- PIDE.spell_checker.get
-        doc_view <- PIDE.document_view(text_area)
+        doc_view <- Document_View.get(text_area)
         rendering = doc_view.get_rendering()
         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
         Text.Info(_, word) <- current_word(text_area, rendering, range)
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -91,7 +91,7 @@
                 GUI_Thread.now {
                   (for {
                     text_area <- JEdit_Lib.jedit_text_areas(buffer)
-                    doc_view <- PIDE.document_view(text_area)
+                    doc_view <- Document_View.get(text_area)
                   } yield doc_view.get_rendering).toStream.headOption
                 }
               else None
diff -r 9eff4c62579a -r c3b42ac0cf81 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Wed Jan 11 22:30:11 2017 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Jan 12 11:17:05 2017 +0100
@@ -156,7 +156,7 @@
     GUI_Thread.require {}
 
     val name =
-      Document_View(view.getTextArea) match {
+      Document_View.get(view.getTextArea) match {
         case None => Document.Node.Name.empty
         case Some(doc_view) => doc_view.model.node_name
       }