# HG changeset patch
# User wenzelm
# Date 1308424822 -7200
# Node ID 591598bc52bca1a0caf25762af5c487d76a4d785
# Parent  90aec504346179906cf7c1f4504b118b7035850c
convenience functions;

diff -r 90aec5043461 -r 591598bc52bc src/Tools/jEdit/src/plugin.scala
--- 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