more explicit development graph;
authorwenzelm
Mon Feb 27 23:35:11 2012 +0100 (2012-02-27 ago)
changeset 4672354ea872b60ea
parent 46722 d0491ab69c84
child 46726 49cbc06af3e5
more explicit development graph;
src/Pure/PIDE/document.scala
src/Pure/library.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Feb 27 23:30:38 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Feb 27 23:35:11 2012 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5    /** document structure **/
     1.6  
     1.7 -  /* named nodes -- development graph */
     1.8 +  /* individual nodes */
     1.9  
    1.10    type Edit[A, B] = (Node.Name, Node.Edit[A, B])
    1.11    type Edit_Text = Edit[Text.Edit, Text.Perspective]
    1.12 @@ -49,6 +49,11 @@
    1.13          val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
    1.14          Name(node, dir, theory)
    1.15        }
    1.16 +
    1.17 +      object Ordering extends scala.math.Ordering[Name]
    1.18 +      {
    1.19 +        def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
    1.20 +      }
    1.21      }
    1.22      sealed case class Name(node: String, dir: String, theory: String)
    1.23      {
    1.24 @@ -169,13 +174,50 @@
    1.25    }
    1.26  
    1.27  
    1.28 +  /* development graph */
    1.29 +
    1.30 +  object Nodes
    1.31 +  {
    1.32 +    val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
    1.33 +  }
    1.34 +
    1.35 +  final class Nodes private(graph: Graph[Node.Name, Node])
    1.36 +  {
    1.37 +    def get_name(s: String): Option[Node.Name] =
    1.38 +      graph.keys.find(name => name.node == s)
    1.39 +
    1.40 +    def apply(name: Node.Name): Node =
    1.41 +      graph.default_node(name, Node.empty).get_node(name)
    1.42 +
    1.43 +    def + (entry: (Node.Name, Node)): Nodes =
    1.44 +    {
    1.45 +      val (name, node) = entry
    1.46 +      val parents =
    1.47 +        node.header match {
    1.48 +          case Exn.Res(header) =>
    1.49 +            // FIXME official names of yet unknown nodes!?
    1.50 +            for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
    1.51 +          case _ => Nil
    1.52 +        }
    1.53 +      val graph1 =
    1.54 +        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
    1.55 +      val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    1.56 +      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
    1.57 +      new Nodes(graph3.map_node(name, _ => node))
    1.58 +    }
    1.59 +
    1.60 +    def entries: Iterator[(Node.Name, Node)] =
    1.61 +      graph.entries.map({ case (name, (node, _)) => (name, node) })
    1.62 +
    1.63 +    def topological_order: List[Node.Name] = graph.topological_order
    1.64 +  }
    1.65 +
    1.66 +
    1.67  
    1.68    /** versioning **/
    1.69  
    1.70    /* particular document versions */
    1.71  
    1.72 -  type Nodes = Map[Node.Name, Node]
    1.73 -
    1.74    object Version
    1.75    {
    1.76      val init: Version = new Version()
    1.77 @@ -185,20 +227,7 @@
    1.78  
    1.79    final class Version private(
    1.80      val id: Version_ID = no_id,
    1.81 -    val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
    1.82 -  {
    1.83 -    def topological_order: List[Node.Name] =
    1.84 -    {
    1.85 -      val names = nodes.map({ case (name, node) => (name.node -> name) })
    1.86 -      def next(x: Node.Name): List[Node.Name] =
    1.87 -        nodes(x).header match {
    1.88 -          case Exn.Res(header) =>
    1.89 -            for (imp <- header.imports; name <- names.get(imp)) yield(name)
    1.90 -          case Exn.Exn(_) => Nil
    1.91 -        }
    1.92 -      Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
    1.93 -    }
    1.94 -  }
    1.95 +    val nodes: Nodes = Nodes.empty)
    1.96  
    1.97  
    1.98    /* changes of plain text, eventually resulting in document edits */
    1.99 @@ -440,7 +469,7 @@
   1.100        for {
   1.101          (version_id, version) <- versions1.iterator
   1.102          val command_execs = assignments1(version_id).command_execs
   1.103 -        (_, node) <- version.nodes.iterator
   1.104 +        (_, node) <- version.nodes.entries
   1.105          command <- node.commands.iterator
   1.106        } {
   1.107          val id = command.id
     2.1 --- a/src/Pure/library.scala	Mon Feb 27 23:30:38 2012 +0100
     2.2 +++ b/src/Pure/library.scala	Mon Feb 27 23:35:11 2012 +0100
     2.3 @@ -128,26 +128,6 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* graph traversal */
     2.8 -
     2.9 -  def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] =
    2.10 -  {
    2.11 -    type Reached = (List[A], Set[A])
    2.12 -    def reach(reached: Reached, x: A): Reached =
    2.13 -    {
    2.14 -      val (rs, r_set) = reached
    2.15 -      if (r_set(x)) reached
    2.16 -      else {
    2.17 -        val (rs1, r_set1) = reachs((rs, r_set + x), next(x))
    2.18 -        (x :: rs1, r_set1)
    2.19 -      }
    2.20 -    }
    2.21 -    def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach)
    2.22 -
    2.23 -    reachs((Nil, Set.empty), starts)._1.reverse
    2.24 -  }
    2.25 -
    2.26 -
    2.27    /* simple dialogs */
    2.28  
    2.29    private def simple_dialog(kind: Int, default_title: String)
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Feb 27 23:30:38 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Feb 27 23:35:11 2012 +0100
     3.3 @@ -147,18 +147,20 @@
     3.4    {
     3.5      Swing_Thread.now {
     3.6        val snapshot = Isabelle.session.snapshot()
     3.7 -      val names = restriction getOrElse snapshot.version.nodes.keySet
     3.8  
     3.9 +      val iterator =
    3.10 +        restriction match {
    3.11 +          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    3.12 +          case None => snapshot.version.nodes.entries
    3.13 +        }
    3.14        val nodes_status1 =
    3.15 -        (nodes_status /: names)((status, name) => {
    3.16 -          val node = snapshot.version.nodes(name)
    3.17 -          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
    3.18 -        })
    3.19 +        (nodes_status /: iterator)({ case (status, (name, node)) =>
    3.20 +            status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    3.21  
    3.22        if (nodes_status != nodes_status1) {
    3.23          nodes_status = nodes_status1
    3.24          status.listData =
    3.25 -          snapshot.version.topological_order.filter(
    3.26 +          snapshot.version.nodes.topological_order.filter(
    3.27              (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
    3.28        }
    3.29      }