src/Tools/VSCode/src/server.scala
changeset 64720 8cc2d7c4ada1
parent 64717 d2b50eb3d9ab
child 64722 6df73de0d3c7
equal deleted inserted replaced
64719:55c871fc39e3 64720:8cc2d7c4ada1
   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")