equal
deleted
inserted
replaced
71 |
71 |
72 class VSCode_Resources( |
72 class VSCode_Resources( |
73 val options: Options, |
73 val options: Options, |
74 session_base_info: Sessions.Base_Info, |
74 session_base_info: Sessions.Base_Info, |
75 log: Logger = No_Logger) |
75 log: Logger = No_Logger) |
76 extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log) |
76 extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log) |
77 { |
77 { |
78 resources => |
78 resources => |
79 |
79 |
80 private val state = Synchronized(VSCode_Resources.State()) |
80 private val state = Synchronized(VSCode_Resources.State()) |
81 |
81 |