equal
deleted
inserted
replaced
33 pending_output: Set[Document.Node.Name] = Set.empty) |
33 pending_output: Set[Document.Node.Name] = Set.empty) |
34 } |
34 } |
35 |
35 |
36 class VSCode_Resources( |
36 class VSCode_Resources( |
37 val options: Options, |
37 val options: Options, |
|
38 val text_length: Text.Length, |
38 loaded_theories: Set[String], |
39 loaded_theories: Set[String], |
39 known_theories: Map[String, Document.Node.Name], |
40 known_theories: Map[String, Document.Node.Name], |
40 base_syntax: Outer_Syntax) |
41 base_syntax: Outer_Syntax) |
41 extends Resources(loaded_theories, known_theories, base_syntax) |
42 extends Resources(loaded_theories, known_theories, base_syntax) |
42 { |
43 { |