equal
deleted
inserted
replaced
62 |
62 |
63 def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value) |
63 def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value) |
64 |
64 |
65 val rich_text_area = |
65 val rich_text_area = |
66 new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), |
66 new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), |
67 caret_visible = true, enable_hovering = false) |
67 () => None, caret_visible = true, enable_hovering = false) |
68 |
68 |
69 |
69 |
70 /* perspective */ |
70 /* perspective */ |
71 |
71 |
72 def perspective(snapshot: Document.Snapshot): Text.Perspective = |
72 def perspective(snapshot: Document.Snapshot): Text.Perspective = |