src/Tools/jEdit/src/jedit_resources.scala
changeset 64854 f5aa712e6250
parent 64841 d53696aed874
child 64856 5e9bf964510a
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 19:34:16 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 20:26:59 2017 +0100
     1.3 @@ -23,15 +23,10 @@
     1.4  
     1.5  object JEdit_Resources
     1.6  {
     1.7 -  val empty: JEdit_Resources =
     1.8 -    new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
     1.9 +  val empty: JEdit_Resources = new JEdit_Resources(Build.Session_Content.empty)
    1.10  }
    1.11  
    1.12 -class JEdit_Resources(
    1.13 -    loaded_theories: Set[String],
    1.14 -    known_theories: Map[String, Document.Node.Name],
    1.15 -    base_syntax: Outer_Syntax)
    1.16 -  extends Resources(loaded_theories, known_theories, base_syntax)
    1.17 +class JEdit_Resources(base: Build.Session_Content) extends Resources(base)
    1.18  {
    1.19    /* document node name */
    1.20