src/Tools/jEdit/src/document_view.scala
changeset 64817 0bb6b582bb4f
parent 64799 c0c648911f1a
child 64882 c3b42ac0cf81
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Jan 07 11:22:13 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Jan 07 14:34:53 2017 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
     1.8 +  def init(model: Buffer_Model, text_area: JEditTextArea): Document_View =
     1.9    {
    1.10      exit(text_area)
    1.11      val doc_view = new Document_View(model, text_area)
    1.12 @@ -56,7 +56,7 @@
    1.13  }
    1.14  
    1.15  
    1.16 -class Document_View(val model: Document_Model, val text_area: JEditTextArea)
    1.17 +class Document_View(val model: Buffer_Model, val text_area: JEditTextArea)
    1.18  {
    1.19    private val session = model.session
    1.20