equal
deleted
inserted
replaced
33 } |
33 } |
34 |
34 |
35 class VSCode_Resources( |
35 class VSCode_Resources( |
36 val options: Options, |
36 val options: Options, |
37 val text_length: Text.Length, |
37 val text_length: Text.Length, |
38 base: Build.Session_Content, |
38 base: Sessions.Base, |
39 log: Logger = No_Logger) extends Resources(base, log) |
39 log: Logger = No_Logger) extends Resources(base, log) |
40 { |
40 { |
41 private val state = Synchronized(VSCode_Resources.State()) |
41 private val state = Synchronized(VSCode_Resources.State()) |
42 |
42 |
43 |
43 |