# HG changeset patch # User wenzelm # Date 1316293443 -7200 # Node ID 9476c856c4b945cc965425f8720c2c4b9c869cf4 # Parent 86e4916825ee0f7b6bbcb6bafb52dc48c4d13367 Document.Node.Name convenience; diff -r 86e4916825ee -r 9476c856c4b9 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Sep 17 22:13:15 2011 +0200 +++ b/src/Pure/PIDE/command.scala Sat Sep 17 23:04:03 2011 +0200 @@ -80,7 +80,7 @@ /* dummy commands */ def unparsed(source: String): Command = - new Command(Document.no_id, Document.Node.Name("", "", ""), + new Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source))) def span(node_name: Document.Node.Name, toks: List[Token]): Command = diff -r 86e4916825ee -r 9476c856c4b9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Sep 17 22:13:15 2011 +0200 +++ b/src/Pure/PIDE/document.scala Sat Sep 17 23:04:03 2011 +0200 @@ -42,6 +42,13 @@ object Name { val empty = Name("", "", "") + def apply(path: Path): Name = + { + val node = path.implode + val dir = path.dir.implode + val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path) + Name(node, dir, theory) + } } sealed case class Name(node: String, dir: String, theory: String) {