src/Pure/PIDE/document.scala
changeset 44960 640c2b957f16
parent 44959 9476c856c4b9
child 45243 27466646a7a3
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Sep 17 23:04:03 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Sep 18 00:05:22 2011 +0200
     1.3 @@ -173,6 +173,20 @@
     1.4  
     1.5    type Nodes = Map[Node.Name, Node]
     1.6    sealed case class Version(val id: Version_ID, val nodes: Nodes)
     1.7 +  {
     1.8 +    def topological_order: List[Node.Name] =
     1.9 +    {
    1.10 +      val names = nodes.map({ case (name, node) => (name.node -> name) })
    1.11 +      def next(x: Node.Name): List[Node.Name] =
    1.12 +        nodes(x).header match {
    1.13 +          case Exn.Res(header) =>
    1.14 +            for (imp <- header.imports; name <- names.get(imp)) yield(name)
    1.15 +          case Exn.Exn(_) => Nil
    1.16 +        }
    1.17 +      Library.topological_order(next,
    1.18 +        Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
    1.19 +    }
    1.20 +  }
    1.21  
    1.22  
    1.23    /* changes of plain text, eventually resulting in document edits */