src/Tools/VSCode/src/vscode_resources.scala
changeset 64706 3ebf9f8299df
parent 64704 08c2d80428ff
child 64707 7157685b71e3
equal deleted inserted replaced
64704:08c2d80428ff 64706:3ebf9f8299df
    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 {