--- 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
--- 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) =
{
--- 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)
--- 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()
--- 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)
--- 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)
--- 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")
}
--- 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)
--- 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
--- 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
}