graph traversal in topological order;
authorwenzelm
Sun Sep 18 00:05:22 2011 +0200 (2011-09-18 ago)
changeset 44960640c2b957f16
parent 44959 9476c856c4b9
child 44961 5b8d39b1360e
graph traversal in topological order;
Session.snapshot() with sensible defaults;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/library.scala
src/Tools/jEdit/src/session_dockable.scala
     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 */
     2.1 --- a/src/Pure/System/session.scala	Sat Sep 17 23:04:03 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sun Sep 18 00:05:22 2011 +0200
     2.3 @@ -107,7 +107,8 @@
     2.4    private val global_state = new Volatile(Document.State.init)
     2.5    def current_state(): Document.State = global_state()
     2.6  
     2.7 -  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
     2.8 +  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
     2.9 +      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    2.10      global_state().snapshot(name, pending_edits)
    2.11  
    2.12  
     3.1 --- a/src/Pure/library.scala	Sat Sep 17 23:04:03 2011 +0200
     3.2 +++ b/src/Pure/library.scala	Sun Sep 18 00:05:22 2011 +0200
     3.3 @@ -139,6 +139,26 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* graph traversal */
     3.8 +
     3.9 +  def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] =
    3.10 +  {
    3.11 +    type Reached = (List[A], Set[A])
    3.12 +    def reach(reached: Reached, x: A): Reached =
    3.13 +    {
    3.14 +      val (rs, r_set) = reached
    3.15 +      if (r_set(x)) reached
    3.16 +      else {
    3.17 +        val (rs1, r_set1) = reachs((rs, r_set + x), next(x))
    3.18 +        (x :: rs1, r_set1)
    3.19 +      }
    3.20 +    }
    3.21 +    def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach)
    3.22 +
    3.23 +    reachs((Nil, Set.empty), starts)._1.reverse
    3.24 +  }
    3.25 +
    3.26 +
    3.27    /* simple dialogs */
    3.28  
    3.29    private def simple_dialog(kind: Int, default_title: String)
     4.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 23:04:03 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 00:05:22 2011 +0200
     4.3 @@ -138,20 +138,20 @@
     4.4    {
     4.5      Swing_Thread.now {
     4.6        // FIXME correlation to changed_nodes!?
     4.7 -      val state = Isabelle.session.current_state()
     4.8 -      val version = state.recent_stable.version.get_finished
     4.9 +      val snapshot = Isabelle.session.snapshot()
    4.10  
    4.11        var nodes_status1 = nodes_status
    4.12        for {
    4.13          name <- changed_nodes
    4.14 -        node <- version.nodes.get(name)
    4.15 -        val status = Isar_Document.node_status(state, version, node)
    4.16 +        node <- snapshot.version.nodes.get(name)
    4.17 +        val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
    4.18        } nodes_status1 += (name -> status)
    4.19  
    4.20        if (nodes_status != nodes_status1) {
    4.21          nodes_status = nodes_status1
    4.22          status.listData =
    4.23 -          Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    4.24 +          snapshot.version.topological_order.filter(
    4.25 +            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
    4.26        }
    4.27      }
    4.28    }