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 base = Sessions.session_base(options, session_name, session_dirs) |
228 val session_base = Sessions.session_base(options, session_name, session_dirs) |
229 val resources = new VSCode_Resources(options, base, log) |
229 val resources = new VSCode_Resources(options, session_base, log) |
230 { |
230 { |
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 } |