src/Tools/jEdit/src/plugin.scala
changeset 43449 591598bc52bc
parent 43443 5d9693c2337e
child 43452 5cf548485529
--- a/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 21:03:52 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 21:20:22 2011 +0200
@@ -191,6 +191,12 @@
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
 
+  /* document model and view */
+
+  def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
+  def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
+
+
   /* dockable windows */
 
   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager