equal
deleted
inserted
replaced
99 |
99 |
100 /* activation */ |
100 /* activation */ |
101 |
101 |
102 def activate_buffer(buffer: Buffer) |
102 def activate_buffer(buffer: Buffer) |
103 { |
103 { |
|
104 session.start(Isabelle.isabelle_args()) |
104 val model = Document_Model.init(session, buffer) |
105 val model = Document_Model.init(session, buffer) |
105 for (text_area <- jedit_text_areas(buffer)) |
106 for (text_area <- jedit_text_areas(buffer)) |
106 Document_View.init(model, text_area) |
107 Document_View.init(model, text_area) |
107 |
|
108 session.start(Isabelle.isabelle_args()) |
|
109 // FIXME theory_view.activate() |
|
110 session.begin_document(buffer.getName) |
|
111 } |
108 } |
112 |
109 |
113 def deactivate_buffer(buffer: Buffer) |
110 def deactivate_buffer(buffer: Buffer) |
114 { |
111 { |
115 session.stop() // FIXME not yet |
112 session.stop() // FIXME not yet |