# HG changeset patch
# User wenzelm
# Date 1260904807 -3600
# Node ID 3779c54a2d213739c14a8a4ef3b120122168b83e
# Parent  0feac35069c67cd9fa96780b7965881703c9dc28
direct apply for Document_Model and Document_View;

diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -32,7 +32,7 @@
     model
   }
 
-  def get(buffer: Buffer): Option[Document_Model] =
+  def apply(buffer: Buffer): Option[Document_Model] =
   {
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
@@ -42,7 +42,7 @@
 
   def exit(buffer: Buffer)
   {
-    get(buffer) match {
+    apply(buffer) match {
       case None => error("No document model for buffer: " + buffer)
       case Some(model) =>
         model.deactivate()
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -46,7 +46,7 @@
     doc_view
   }
 
-  def get(text_area: TextArea): Option[Document_View] =
+  def apply(text_area: TextArea): Option[Document_View] =
   {
     text_area.getClientProperty(key) match {
       case doc_view: Document_View => Some(doc_view)
@@ -56,7 +56,7 @@
 
   def exit(text_area: TextArea)
   {
-    get(text_area) match {
+    apply(text_area) match {
       case None => error("No document view for text area: " + text_area)
       case Some(doc_view) =>
         doc_view.deactivate()
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/history_dockable.scala
--- a/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -23,7 +23,7 @@
     preferredSize = new Dimension(500, 250)
 
   def get_versions() =
-    Document_Model.get(view.getBuffer) match {
+    Document_Model(view.getBuffer) match {
       case None => Nil
       case Some(model) => model.changes
     }
@@ -36,9 +36,9 @@
   listenTo(list.selection)
   reactions += {
     case ListSelectionChanged(source, range, false) =>
-      Document_Model.get(view.getBuffer).map(_.set_version(list.listData(range.start)))
+      Document_Model(view.getBuffer).map(_.set_version(list.listData(range.start)))
   }
 
-  if (Document_Model.get(view.getBuffer).isDefined)
+  if (Document_Model(view.getBuffer).isDefined)
     Isabelle.session.document_change += (_ => list.listData = get_versions())
 }
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -45,7 +45,7 @@
 {
 	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
 	{
-    Document_Model.get(buffer) match {
+    Document_Model(buffer) match {
       case Some(model) =>
         val document = model.current_document()
         val offset = model.from_current(document, original_offset)
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -40,7 +40,7 @@
     val root = data.root
     data.getAsset(root).setEnd(buffer.getLength)
 
-    Document_Model.get(buffer) match {
+    Document_Model(buffer) match {
       case Some(model) =>
         val document = model.current_document()
         for (command <- document.commands if !stopped) {
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -42,7 +42,7 @@
     loop {
       react {
         case cmd: Command =>
-          Document_Model.get(view.getBuffer) match {
+          Document_Model(view.getBuffer) match {
             case None =>
             case Some(model) =>
               val body =
diff -r 0feac35069c6 -r 3779c54a2d21 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 20:15:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 20:20:07 2009 +0100
@@ -122,12 +122,12 @@
   def switch_active(view: View) =
   {
     val buffer = view.getBuffer
-    if (Document_Model.get(buffer).isDefined) deactivate_buffer(buffer)
+    if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
     else activate_buffer(buffer)
   }
 
   def is_active(view: View): Boolean =
-    Document_Model.get(view.getBuffer).isDefined
+    Document_Model(view.getBuffer).isDefined
 }
 
 
@@ -145,14 +145,14 @@
 
         def init_view()
         {
-          Document_Model.get(buffer) match {
+          Document_Model(buffer) match {
             case Some(model) => Document_View.init(model, text_area)
             case None =>
           }
         }
         def exit_view()
         {
-          if (Document_View.get(text_area).isDefined)
+          if (Document_View(text_area).isDefined)
             Document_View.exit(text_area)
         }
         msg.getWhat match {