equal
deleted
inserted
replaced
320 |
320 |
321 PIDE.editor.hyperlink_position(true, Document.Snapshot.init, |
321 PIDE.editor.hyperlink_position(true, Document.Snapshot.init, |
322 JEdit_Sessions.session_info().open_root).foreach(_.follow(view)) |
322 JEdit_Sessions.session_info().open_root).foreach(_.follow(view)) |
323 |
323 |
324 case msg: BufferUpdate |
324 case msg: BufferUpdate |
325 if msg.getWhat == BufferUpdate.LOADED || |
325 if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING => |
326 msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || |
326 if (msg.getBuffer != null) PIDE.exit_models(List(msg.getBuffer)) |
327 msg.getWhat == BufferUpdate.CLOSING => |
327 |
328 |
328 case msg: BufferUpdate |
329 if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null) |
329 if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED => |
330 PIDE.exit_models(List(msg.getBuffer)) |
|
331 |
|
332 if (PIDE.session.is_ready) { |
330 if (PIDE.session.is_ready) { |
333 delay_init.invoke() |
331 delay_init.invoke() |
334 delay_load.invoke() |
332 delay_load.invoke() |
335 } |
333 } |
336 |
334 |