| changeset 50199 | 6d04e2422769 |
| parent 49843 | afddf4e26fac |
| child 50205 | 788c8263e634 |
--- a/src/Tools/jEdit/src/document_view.scala Sun Nov 25 17:15:21 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Sun Nov 25 18:47:33 2012 +0100 @@ -67,8 +67,7 @@ { private val session = model.session - def get_rendering(): Isabelle_Rendering = - Isabelle_Rendering(model.snapshot(), Isabelle.options.value) + def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value) val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)