clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
authorwenzelm
Thu Mar 01 11:28:33 2012 +0100 (2012-03-01)
changeset 467396024353549ca
parent 46738 1d2cbcc50fb2
child 46740 852baa599351
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
tuned;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Feb 29 23:31:35 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 01 11:28:33 2012 +0100
     1.3 @@ -212,15 +212,15 @@
     1.4          |> touch_node name
     1.5      | Header header =>
     1.6          let
     1.7 -          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
     1.8 +          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
     1.9            val nodes1 = nodes
    1.10              |> default_node name
    1.11 -            |> fold default_node parents;
    1.12 +            |> fold default_node imports;
    1.13            val nodes2 = nodes1
    1.14              |> Graph.Keys.fold
    1.15                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.16            val (header', nodes3) =
    1.17 -            (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.18 +            (header, Graph.add_deps_acyclic (name, imports) nodes2)
    1.19                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.20          in Graph.map_node name (set_header header') nodes3 end
    1.21          |> touch_node name
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Feb 29 23:31:35 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 01 11:28:33 2012 +0100
     2.3 @@ -188,15 +188,15 @@
     2.4      def + (entry: (Node.Name, Node)): Nodes =
     2.5      {
     2.6        val (name, node) = entry
     2.7 -      val parents =
     2.8 +      val imports =
     2.9          node.header match {
    2.10 -          case Exn.Res(deps) => deps.imports.filter(_.dir != "")  // FIXME more specific filter
    2.11 +          case Exn.Res(deps) => deps.imports
    2.12            case _ => Nil
    2.13          }
    2.14        val graph1 =
    2.15 -        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
    2.16 +        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    2.17        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    2.18 -      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
    2.19 +      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
    2.20        new Nodes(graph3.map_node(name, _ => node))
    2.21      }
    2.22  
     3.1 --- a/src/Pure/System/session.scala	Wed Feb 29 23:31:35 2012 +0100
     3.2 +++ b/src/Pure/System/session.scala	Thu Mar 01 11:28:33 2012 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Session(val thy_load: Thy_Load = new Thy_Load)
     3.8 +class Session(thy_load: Thy_Load = new Thy_Load)
     3.9  {
    3.10    /* real time parameters */  // FIXME properties or settings (!?)
    3.11  
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 23:31:35 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 11:28:33 2012 +0100
     4.3 @@ -64,7 +64,7 @@
     4.4    {
     4.5      Swing_Thread.require()
     4.6      if (Isabelle.jedit_buffer(name.node) == Some(buffer))
     4.7 -      Exn.capture { session.thy_load.check_thy(name) }
     4.8 +      Exn.capture { Isabelle.thy_load.check_thy(name) }
     4.9      else Exn.Exn(ERROR("Bad theory header"))  // FIXME odd race condition!?
    4.10    }
    4.11  
     5.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Wed Feb 29 23:31:35 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Mar 01 11:28:33 2012 +0100
     5.3 @@ -155,7 +155,8 @@
     5.4          }
     5.5        val nodes_status1 =
     5.6          (nodes_status /: iterator)({ case (status, (name, node)) =>
     5.7 -            status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
     5.8 +            if (Isabelle.thy_load.is_loaded(name.theory)) status
     5.9 +            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    5.10  
    5.11        if (nodes_status != nodes_status1) {
    5.12          nodes_status = nodes_status1