src/Tools/jEdit/src/jedit_resources.scala
changeset 56801 8dd9df88f647
parent 56666 229309cbc508
child 56823 37be55461dbe
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 13:11:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 22:34:11 2014 +0200
     1.3 @@ -19,8 +19,11 @@
     1.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     1.5  
     1.6  
     1.7 -class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
     1.8 -  extends Resources(loaded_theories, base_syntax)
     1.9 +class JEdit_Resources(
    1.10 +    loaded_theories: Set[String],
    1.11 +    known_theories: Map[String, Document.Node.Name],
    1.12 +    base_syntax: Outer_Syntax)
    1.13 +  extends Resources(loaded_theories, known_theories, base_syntax)
    1.14  {
    1.15    /* document node names */
    1.16