equal
deleted
inserted
replaced
125 private val dynamic_output = Dynamic_Output(server) |
125 private val dynamic_output = Dynamic_Output(server) |
126 |
126 |
127 |
127 |
128 /* input from client or file-system */ |
128 /* input from client or file-system */ |
129 |
129 |
|
130 private val file_watcher: File_Watcher = |
|
131 File_Watcher(sync_documents, options.seconds("vscode_load_delay")) |
|
132 |
130 private val delay_input: Delay = |
133 private val delay_input: Delay = |
131 Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) |
134 Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) |
132 { resources.flush_input(session, channel) } |
135 { resources.flush_input(session, channel) } |
133 |
136 |
134 private val delay_load: Delay = |
137 private val delay_load: Delay = |
136 val (invoke_input, invoke_load) = |
139 val (invoke_input, invoke_load) = |
137 resources.resolve_dependencies(session, editor, file_watcher) |
140 resources.resolve_dependencies(session, editor, file_watcher) |
138 if (invoke_input) delay_input.invoke() |
141 if (invoke_input) delay_input.invoke() |
139 if (invoke_load) delay_load.invoke() |
142 if (invoke_load) delay_load.invoke() |
140 } |
143 } |
141 |
|
142 private val file_watcher = |
|
143 File_Watcher(sync_documents, options.seconds("vscode_load_delay")) |
|
144 |
144 |
145 private def close_document(file: JFile): Unit = |
145 private def close_document(file: JFile): Unit = |
146 { |
146 { |
147 if (resources.close_model(file)) { |
147 if (resources.close_model(file)) { |
148 file_watcher.register_parent(file) |
148 file_watcher.register_parent(file) |