Document.Node.Name convenience;
authorwenzelm
Sat Sep 17 23:04:03 2011 +0200 (2011-09-17)
changeset 449599476c856c4b9
parent 44958 86e4916825ee
child 44960 640c2b957f16
Document.Node.Name convenience;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Sep 17 22:13:15 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Sep 17 23:04:03 2011 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    /* dummy commands */
     1.5  
     1.6    def unparsed(source: String): Command =
     1.7 -    new Command(Document.no_id, Document.Node.Name("", "", ""),
     1.8 +    new Command(Document.no_id, Document.Node.Name.empty,
     1.9        List(Token(Token.Kind.UNPARSED, source)))
    1.10  
    1.11    def span(node_name: Document.Node.Name, toks: List[Token]): Command =
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 17 22:13:15 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Sep 17 23:04:03 2011 +0200
     2.3 @@ -42,6 +42,13 @@
     2.4      object Name
     2.5      {
     2.6        val empty = Name("", "", "")
     2.7 +      def apply(path: Path): Name =
     2.8 +      {
     2.9 +        val node = path.implode
    2.10 +        val dir = path.dir.implode
    2.11 +        val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    2.12 +        Name(node, dir, theory)
    2.13 +      }
    2.14      }
    2.15      sealed case class Name(node: String, dir: String, theory: String)
    2.16      {