equal
deleted
inserted
replaced
43 doc_view.deactivate() |
43 doc_view.deactivate() |
44 text_area.putClientProperty(key, null) |
44 text_area.putClientProperty(key, null) |
45 } |
45 } |
46 } |
46 } |
47 |
47 |
48 def init(model: Document_Model, text_area: JEditTextArea): Document_View = |
48 def init(model: Buffer_Model, text_area: JEditTextArea): Document_View = |
49 { |
49 { |
50 exit(text_area) |
50 exit(text_area) |
51 val doc_view = new Document_View(model, text_area) |
51 val doc_view = new Document_View(model, text_area) |
52 text_area.putClientProperty(key, doc_view) |
52 text_area.putClientProperty(key, doc_view) |
53 doc_view.activate() |
53 doc_view.activate() |
54 doc_view |
54 doc_view |
55 } |
55 } |
56 } |
56 } |
57 |
57 |
58 |
58 |
59 class Document_View(val model: Document_Model, val text_area: JEditTextArea) |
59 class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) |
60 { |
60 { |
61 private val session = model.session |
61 private val session = model.session |
62 |
62 |
63 def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value) |
63 def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value) |
64 |
64 |