src/Pure/PIDE/document.scala
changeset 66195 bb886f13623a
parent 66150 c2e19b9e1398
child 66382 6392766f3c25
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jun 26 11:07:48 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jun 26 15:57:20 2017 +0200
     1.3 @@ -123,6 +123,7 @@
     1.4        override def toString: String = if (is_theory) theory else node
     1.5  
     1.6        def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     1.7 +      def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     1.8      }
     1.9  
    1.10