equal
deleted
inserted
replaced
65 |
65 |
66 class Document_View(val model: Document_Model, val text_area: JEditTextArea) |
66 class Document_View(val model: Document_Model, val text_area: JEditTextArea) |
67 { |
67 { |
68 private val session = model.session |
68 private val session = model.session |
69 |
69 |
70 def get_rendering(): Isabelle_Rendering = |
70 def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value) |
71 Isabelle_Rendering(model.snapshot(), Isabelle.options.value) |
|
72 |
71 |
73 val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false) |
72 val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false) |
74 |
73 |
75 |
74 |
76 /* perspective */ |
75 /* perspective */ |