equal
deleted
inserted
replaced
92 } |
92 } |
93 |
93 |
94 private def uninstall(view: View) |
94 private def uninstall(view: View) |
95 { |
95 { |
96 val buffer = view.getBuffer |
96 val buffer = view.getBuffer |
97 mapping(buffer).deactivate |
97 Isabelle.session.stop() |
|
98 mapping(buffer).deactivate() |
98 mapping -= buffer |
99 mapping -= buffer |
99 } |
100 } |
100 |
101 |
101 def switch_active(view: View) = |
102 def switch_active(view: View) = |
102 if (mapping.isDefinedAt(view.getBuffer)) uninstall(view) |
103 if (mapping.isDefinedAt(view.getBuffer)) uninstall(view) |