--- a/src/Pure/PIDE/document.scala Mon Apr 03 12:49:13 2017 +0200
+++ b/src/Pure/PIDE/document.scala Mon Apr 03 13:39:13 2017 +0200
@@ -98,6 +98,7 @@
object Name
{
val empty = Name("")
+ def theory(theory: String): Name = Name(theory, "", theory)
object Ordering extends scala.math.Ordering[Name]
{