1.1 --- a/src/Tools/VSCode/src/server.scala Sat Dec 31 11:45:24 2016 +0100
1.2 +++ b/src/Tools/VSCode/src/server.scala Sat Dec 31 14:20:50 2016 +0100
1.3 @@ -186,8 +186,8 @@
1.4 try {
1.5 val content = Build.session_content(options, false, session_dirs, session_name)
1.6 val resources =
1.7 - new VSCode_Resources(
1.8 - options, text_length, content.loaded_theories, content.known_theories, content.syntax)
1.9 + new VSCode_Resources(options, text_length, content.loaded_theories,
1.10 + content.known_theories, content.syntax, log)
1.11
1.12 Some(new Session(resources) {
1.13 override def output_delay = options.seconds("editor_output_delay")