equal
deleted
inserted
replaced
78 } yield doc_view.get |
78 } yield doc_view.get |
79 |
79 |
80 def exit_models(buffers: List[Buffer]) |
80 def exit_models(buffers: List[Buffer]) |
81 { |
81 { |
82 Swing_Thread.now { |
82 Swing_Thread.now { |
|
83 PIDE.editor.flush() |
83 buffers.foreach(buffer => |
84 buffers.foreach(buffer => |
84 JEdit_Lib.buffer_lock(buffer) { |
85 JEdit_Lib.buffer_lock(buffer) { |
85 JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) |
86 JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) |
86 Document_Model.exit(buffer) |
87 Document_Model.exit(buffer) |
87 }) |
88 }) |
89 } |
90 } |
90 |
91 |
91 def init_models(buffers: List[Buffer]) |
92 def init_models(buffers: List[Buffer]) |
92 { |
93 { |
93 Swing_Thread.now { |
94 Swing_Thread.now { |
|
95 PIDE.editor.flush() |
94 val init_edits = |
96 val init_edits = |
95 (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) => |
97 (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) => |
96 JEdit_Lib.buffer_lock(buffer) { |
98 JEdit_Lib.buffer_lock(buffer) { |
97 val (model_edits, opt_model) = |
99 val (model_edits, opt_model) = |
98 thy_load.buffer_node_name(buffer) match { |
100 thy_load.buffer_node_name(buffer) match { |