src/Tools/VSCode/src/server.scala
changeset 65272 7611c55c39d0
parent 65264 7e6ecd04b5fe
child 65317 b9f5cd845616
equal deleted inserted replaced
65271:9dcd6574383b 65272:7611c55c39d0
   231             override def commit(change: Session.Change): Unit =
   231             override def commit(change: Session.Change): Unit =
   232               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
   232               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
   233                 delay_load.invoke()
   233                 delay_load.invoke()
   234           }
   234           }
   235 
   235 
   236         Some(new Session(options, resources))
   236         val session_options = options.bool("editor_output_state") = true
       
   237         Some(new Session(session_options, resources))
   237       }
   238       }
   238       catch { case ERROR(msg) => reply(msg); None }
   239       catch { case ERROR(msg) => reply(msg); None }
   239 
   240 
   240     for (session <- try_session) {
   241     for (session <- try_session) {
   241       session_.change(_ => Some(session))
   242       session_.change(_ => Some(session))