tuned;
authorwenzelm
Fri Apr 21 11:21:59 2017 +0200 (2017-04-21)
changeset 6552953fd6cf53ec2
parent 65528 d15d302da7f0
child 65530 09c00a304c00
tuned;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Apr 21 10:59:07 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Apr 21 11:21:59 2017 +0200
     1.3 @@ -93,8 +93,8 @@
     1.4          }
     1.5      }
     1.6  
     1.7 -  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
     1.8 -    import_name(theory_qualifier(node_name), node_name.master_dir, s)
     1.9 +  def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
    1.10 +    import_name(theory_qualifier(name), name.master_dir, s)
    1.11  
    1.12    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.13    {