author | wenzelm |
Wed, 15 Mar 2017 21:52:04 +0100 | |
changeset 65272 | 7611c55c39d0 |
parent 65271 | 9dcd6574383b |
child 65273 | 917ae0ba03a2 |
child 65275 | 50f956a1ac3f |
--- a/src/Tools/VSCode/src/server.scala Wed Mar 15 20:39:23 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Mar 15 21:52:04 2017 +0100 @@ -233,7 +233,8 @@ delay_load.invoke() } - Some(new Session(options, resources)) + val session_options = options.bool("editor_output_state") = true + Some(new Session(session_options, resources)) } catch { case ERROR(msg) => reply(msg); None }