equal
deleted
inserted
replaced
184 |
184 |
185 val try_session = |
185 val try_session = |
186 try { |
186 try { |
187 val content = Build.session_content(options, false, session_dirs, session_name) |
187 val content = Build.session_content(options, false, session_dirs, session_name) |
188 val resources = |
188 val resources = |
189 new VSCode_Resources( |
189 new VSCode_Resources(options, text_length, content.loaded_theories, |
190 options, text_length, content.loaded_theories, content.known_theories, content.syntax) |
190 content.known_theories, content.syntax, log) |
191 |
191 |
192 Some(new Session(resources) { |
192 Some(new Session(resources) { |
193 override def output_delay = options.seconds("editor_output_delay") |
193 override def output_delay = options.seconds("editor_output_delay") |
194 override def prune_delay = options.seconds("editor_prune_delay") |
194 override def prune_delay = options.seconds("editor_prune_delay") |
195 override def syslog_limit = options.int("editor_syslog_limit") |
195 override def syslog_limit = options.int("editor_syslog_limit") |