equal
deleted
inserted
replaced
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() |