changeset 70539 | 30b3c58a1933 |
parent 70284 | 3e17c3a5fd39 |
child 70636 | a56eab490f4e |
--- a/src/Pure/PIDE/document.scala Thu Aug 15 16:57:09 2019 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 15 18:21:12 2019 +0200 @@ -390,6 +390,9 @@ def iterator: Iterator[(Node.Name, Node)] = graph.iterator.map({ case (name, (node, _)) => (name, node) }) + def theory_name(theory: String): Option[Node.Name] = + graph.keys_iterator.find(name => name.theory == theory) + def commands_loading(file_name: Node.Name): List[Command] = (for { (_, node) <- iterator