src/Tools/VSCode/src/server.scala
changeset 65512 9fd620f2fa7d
parent 65361 ecefb68dc21d
child 65922 d2f19f05c0e9
equal deleted inserted replaced
65511:ea42dfd95ec8 65512:9fd620f2fa7d
   223           {
   223           {
   224             progress.echo(fail_msg); error(fail_msg)
   224             progress.echo(fail_msg); error(fail_msg)
   225           }
   225           }
   226         }
   226         }
   227 
   227 
   228         val session_base = Sessions.session_base(options, session_name, session_dirs)
   228         val session_base =
       
   229           Sessions.session_base(options, session_name, dirs = session_dirs, all_known = true)
   229         val resources = new VSCode_Resources(options, session_base, log)
   230         val resources = new VSCode_Resources(options, session_base, log)
   230           {
   231           {
   231             override def commit(change: Session.Change): Unit =
   232             override def commit(change: Session.Change): Unit =
   232               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
   233               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
   233                 delay_load.invoke()
   234                 delay_load.invoke()