src/Tools/jEdit/src/document_view.scala
changeset 64621 7116f2634e32
parent 64524 e6a3c55b929b
child 64799 c0c648911f1a
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Dec 20 18:11:42 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Dec 20 21:35:56 2016 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4  {
     1.5    private val session = model.session
     1.6  
     1.7 -  def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
     1.8 +  def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value)
     1.9  
    1.10    val rich_text_area =
    1.11      new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,