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