equal
deleted
inserted
replaced
35 } |
35 } |
36 |
36 |
37 class VSCode_Rendering( |
37 class VSCode_Rendering( |
38 val model: Document_Model, |
38 val model: Document_Model, |
39 snapshot: Document.Snapshot, |
39 snapshot: Document.Snapshot, |
40 options: Options, |
|
41 resources: VSCode_Resources) |
40 resources: VSCode_Resources) |
42 extends Rendering(snapshot, options, resources) |
41 extends Rendering(snapshot, resources.options, resources) |
43 { |
42 { |
44 /* diagnostics */ |
43 /* diagnostics */ |
45 |
44 |
46 def diagnostics: List[Text.Info[Command.Results]] = |
45 def diagnostics: List[Text.Info[Command.Results]] = |
47 snapshot.cumulate[Command.Results]( |
46 snapshot.cumulate[Command.Results]( |