proper log;
authorwenzelm
Sat Dec 31 14:20:50 2016 +0100 (2016-12-31)
changeset 647208cc2d7c4ada1
parent 64719 55c871fc39e3
child 64721 4b9c96c3850b
proper log;
src/Tools/VSCode/src/server.scala
     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")