changeset 70716 | a8afe8eb3529 |
parent 70699 | 3eb30d80cee6 |
child 70780 | 034742453594 |
--- a/src/Pure/PIDE/document.scala Mon Sep 16 20:06:25 2019 +0200 +++ b/src/Pure/PIDE/document.scala Mon Sep 16 21:30:30 2019 +0200 @@ -102,8 +102,6 @@ { val empty = Name("") - def loaded_theory(theory: String): Name = Name(theory, "", theory) - object Ordering extends scala.math.Ordering[Name] { def compare(name1: Name, name2: Name): Int = name1.node compare name2.node