141 case msg: EditPaneUpdate => |
141 case msg: EditPaneUpdate => |
142 val edit_pane = msg.getEditPane |
142 val edit_pane = msg.getEditPane |
143 val buffer = edit_pane.getBuffer |
143 val buffer = edit_pane.getBuffer |
144 val text_area = edit_pane.getTextArea |
144 val text_area = edit_pane.getTextArea |
145 |
145 |
|
146 def init_view() |
|
147 { |
|
148 Document_Model.get(buffer) match { |
|
149 case Some(model) => Document_View.init(model, text_area) |
|
150 case None => |
|
151 } |
|
152 } |
|
153 def exit_view() |
|
154 { |
|
155 if (Document_View.get(text_area).isDefined) |
|
156 Document_View.exit(text_area) |
|
157 } |
146 msg.getWhat match { |
158 msg.getWhat match { |
147 case EditPaneUpdate.BUFFER_CHANGED => |
159 case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view() |
148 if (Document_View.get(text_area).isDefined) |
160 case EditPaneUpdate.CREATED => init_view() |
149 Document_View.exit(text_area) |
161 case EditPaneUpdate.DESTROYED => exit_view() |
150 Document_Model.get(buffer) match { |
|
151 case Some(model) => Document_View.init(model, text_area) |
|
152 case None => |
|
153 } |
|
154 |
|
155 case EditPaneUpdate.DESTROYED => |
|
156 if (Document_View.get(text_area).isDefined) |
|
157 Document_View.exit(text_area) |
|
158 |
|
159 case _ => |
162 case _ => |
160 } |
163 } |
161 |
164 |
162 case msg: PropertiesChanged => |
165 case msg: PropertiesChanged => |
163 Isabelle.session.global_settings.event(()) |
166 Isabelle.session.global_settings.event(()) |