# HG changeset patch
# User wenzelm
# Date 1330597713 -3600
# Node ID 6024353549ca0d8a75b1cf9c3947aff00eb10ed5
# Parent  1d2cbcc50fb2844f321757d6181cf7ac353e0b06
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
tuned;

diff -r 1d2cbcc50fb2 -r 6024353549ca src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 01 11:28:33 2012 +0100
@@ -212,15 +212,15 @@
         |> touch_node name
     | Header header =>
         let
-          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
           val nodes1 = nodes
             |> default_node name
-            |> fold default_node parents;
+            |> fold default_node imports;
           val nodes2 = nodes1
             |> Graph.Keys.fold
                 (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
           val (header', nodes3) =
-            (header, Graph.add_deps_acyclic (name, parents) nodes2)
+            (header, Graph.add_deps_acyclic (name, imports) nodes2)
               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
         in Graph.map_node name (set_header header') nodes3 end
         |> touch_node name
diff -r 1d2cbcc50fb2 -r 6024353549ca src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 01 11:28:33 2012 +0100
@@ -188,15 +188,15 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val parents =
+      val imports =
         node.header match {
-          case Exn.Res(deps) => deps.imports.filter(_.dir != "")  // FIXME more specific filter
+          case Exn.Res(deps) => deps.imports
           case _ => Nil
         }
       val graph1 =
-        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
+        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
-      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
+      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
       new Nodes(graph3.map_node(name, _ => node))
     }
 
diff -r 1d2cbcc50fb2 -r 6024353549ca src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Mar 01 11:28:33 2012 +0100
@@ -35,7 +35,7 @@
 }
 
 
-class Session(val thy_load: Thy_Load = new Thy_Load)
+class Session(thy_load: Thy_Load = new Thy_Load)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
diff -r 1d2cbcc50fb2 -r 6024353549ca src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 11:28:33 2012 +0100
@@ -64,7 +64,7 @@
   {
     Swing_Thread.require()
     if (Isabelle.jedit_buffer(name.node) == Some(buffer))
-      Exn.capture { session.thy_load.check_thy(name) }
+      Exn.capture { Isabelle.thy_load.check_thy(name) }
     else Exn.Exn(ERROR("Bad theory header"))  // FIXME odd race condition!?
   }
 
diff -r 1d2cbcc50fb2 -r 6024353549ca src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Mar 01 11:28:33 2012 +0100
@@ -155,7 +155,8 @@
         }
       val nodes_status1 =
         (nodes_status /: iterator)({ case (status, (name, node)) =>
-            status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+            if (Isabelle.thy_load.is_loaded(name.theory)) status
+            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1