src/Tools/jEdit/src/jedit_resources.scala
changeset 60835 6512bb0b1ff4
parent 59691 f6ff19188842
child 60916 a6e2a667b0a8
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 11:39:30 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jul 30 14:02:19 2015 +0200
     1.3 @@ -21,6 +21,12 @@
     1.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     1.5  
     1.6  
     1.7 +object JEdit_Resources
     1.8 +{
     1.9 +  val empty: JEdit_Resources =
    1.10 +    new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
    1.11 +}
    1.12 +
    1.13  class JEdit_Resources(
    1.14      loaded_theories: Set[String],
    1.15      known_theories: Map[String, Document.Node.Name],
    1.16 @@ -119,4 +125,3 @@
    1.17      if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
    1.18    }
    1.19  }
    1.20 -