clarified module Thy_Load;
more precise graph based on Document.Node.Deps with actual Node.Name dependencies;

--- a/src/Pure/PIDE/document.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -35,10 +35,12 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
-  type Node_Header = Exn.Result[Thy_Header]
+  type Node_Header = Exn.Result[Node.Deps]
 
   object Node
   {
+    sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)])
+
     object Name
     {
       val empty = Name("", "", "")
@@ -81,12 +83,6 @@
     case class Header[A, B](header: Node_Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
-    def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
-      header match {
-        case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
-        case exn => exn
-      }
-
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -194,9 +190,7 @@
       val (name, node) = entry
       val parents =
         node.header match {
-          case Exn.Res(header) =>
-            // FIXME official names of yet unknown nodes!?
-            for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
+          case Exn.Res(deps) => deps.imports.filter(_.dir != "")  // FIXME more specific filter
           case _ => Nil
         }
       val graph1 =

--- a/src/Pure/PIDE/protocol.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -211,22 +211,24 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
-      def encode_edit(dir: String)
+      def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
         variant(List(
           { case Document.Node.Clear() => (Nil, Nil) },
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
-          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+          { case Document.Node.Header(Exn.Res(deps)) =>
+              val dir = Isabelle_System.posix_path(name.dir)
+              val imports = deps.imports.map(_.node)
+              val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
               (Nil,
                 triple(pair(string, string), list(string), list(pair(string, bool)))(
-                  (dir, a), b, c)) },
+                  (dir, name.theory), imports, uses)) },
           { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
           { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
       def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
-        val dir = Isabelle_System.posix_path(name.dir)
-        pair(string, encode_edit(dir))(name.node, edit)
+        pair(string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode(edits)) }
     input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Feb 29 23:09:06 2012 +0100
@@ -143,7 +143,7 @@
       Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
         handle ERROR msg =>
           (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
-            tell_file_retracted (Thy_Header.thy_path name))
+            tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
     val _ = Isar.init ();
   in () end;
 

--- a/src/Pure/System/session.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/System/session.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -35,7 +35,7 @@
 }
 
 
-class Session(thy_load: Thy_Load = new Thy_Load)
+class Session(val thy_load: Thy_Load = new Thy_Load)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
@@ -143,20 +143,11 @@
 
   def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
   {
-    def norm_import(s: String): String =
-    {
-      val thy_name = Thy_Header.base_name(s)
-      if (thy_load.is_loaded(thy_name)) thy_name
-      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
-    }
-    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
-
     val header1: Document.Node_Header =
       header match {
-        case Exn.Res(Thy_Header(thy_name, _, _))
-        if (thy_load.is_loaded(thy_name)) =>
-          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
-        case _ => Document.Node.norm_header(norm_import, norm_use, header)
+        case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
+          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
+        case _ => header
       }
     (name, Document.Node.Header(header1))
   }

--- a/src/Pure/Thy/thy_header.ML	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Feb 29 23:09:06 2012 +0100
@@ -8,8 +8,6 @@
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> string -> string * string list * (Path.T * bool) list
-  val thy_path: string -> Path.T
-  val consistent_name: string -> string -> unit
 end;
 
 structure Thy_Header: THY_HEADER =
@@ -67,13 +65,4 @@
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
-
-(* file name *)
-
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun consistent_name name name' =
-  if name = name' then ()
-  else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
-
 end;

--- a/src/Pure/Thy/thy_header.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -37,8 +37,6 @@
   def thy_name(s: String): Option[String] =
     s match { case Thy_Name(name) => Some(name) case _ => None }
 
-  def thy_path(path: Path): Path = path.ext("thy")
-
 
   /* header */
 
@@ -96,18 +94,6 @@
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
-
-
-  /* check */
-
-  def check(name: String, source: CharSequence): Thy_Header =
-  {
-    val header = read(source)
-    val name1 = header.name
-    val path = Path.explode(name)
-    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
-    header
-  }
 }
 
 
@@ -116,10 +102,5 @@
 {
   def map(f: String => String): Thy_Header =
     Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
-
-  def norm_deps(f: String => String, g: String => String): Thy_Header =
-    copy(imports = imports.map(name => f(name)))
-    // FIXME
-    // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
 }
 

--- a/src/Pure/Thy/thy_info.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -24,15 +24,6 @@
 
   /* dependencies */
 
-  def import_name(dir: String, str: String): Document.Node.Name =
-  {
-    val path = Path.explode(str)
-    val node = thy_load.append(dir, Thy_Header.thy_path(path))
-    val dir1 = thy_load.append(dir, path.dir)
-    val theory = path.base.implode
-    Document.Node.Name(node, dir1, theory)
-  }
-
   type Dep = (Document.Node.Name, Document.Node_Header)
   private type Required = (List[Dep], Set[Document.Node.Name])
 
@@ -49,16 +40,16 @@
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
-        val header =
+        val node_deps =
           try { thy_load.check_thy(name) }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name.theory) + required_by(initiators))
           }
-        val imports = header.imports.map(import_name(name.dir, _))
-        val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports)
-        ((name, Exn.Res(header)) :: deps1, seen1)
+        val (deps1, seen1) =
+          require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
+        ((name, Exn.Res(node_deps)) :: deps1, seen1)
       }
       catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
     }

--- a/src/Pure/Thy/thy_load.ML	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Feb 29 23:09:06 2012 +0100
@@ -10,6 +10,7 @@
   val imports_of: theory -> string list
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
   val check_file: Path.T -> Path.T -> Path.T
+  val thy_path: Path.T -> Path.T
   val check_thy: Path.T -> string ->
     {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -75,14 +76,18 @@
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
+val thy_path = Path.ext "thy";
+
 fun check_thy dir name =
   let
-    val master_file = check_file dir (Thy_Header.thy_path name);
+    val path = thy_path (Path.basic name);
+    val master_file = check_file dir path;
     val text = File.read master_file;
     val (name', imports, uses) =
       if name = Context.PureN then (Context.PureN, [], [])
       else Thy_Header.read (Path.position master_file) text;
-    val _ = Thy_Header.consistent_name name name';
+    val _ = name <> name' andalso
+      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
   in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 

--- a/src/Pure/Thy/thy_load.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -29,11 +29,39 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).implode
 
-  def check_thy(name: Document.Node.Name): Thy_Header =
+  def read_header(name: Document.Node.Name): Thy_Header =
   {
     val file = new File(name.node)
     if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     Thy_Header.read(file)
   }
+
+
+  /* theory files */
+
+  def thy_path(path: Path): Path = path.ext("thy")
+
+  private def import_name(dir: String, s: String): Document.Node.Name =
+  {
+    val theory = Thy_Header.base_name(s)
+    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
+    else {
+      val path = Path.explode(s)
+      val node = append(dir, thy_path(path))
+      val dir1 = append(dir, path.dir)
+      Document.Node.Name(node, dir1, theory)
+    }
+  }
+
+  def check_thy(name: Document.Node.Name): Document.Node.Deps =
+  {
+    val header = read_header(name)
+    val name1 = header.name
+    val imports = header.imports.map(import_name(name.dir, _))
+    val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+    if (name.theory != name1)
+      error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
+    Document.Node.Deps(imports, uses)
+  }
 }
 

--- a/src/Pure/Thy/thy_syntax.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -258,7 +258,7 @@
           val node = nodes(name)
           val update_header =
             (node.header, header) match {
-              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
               case _ => true
             }
           if (update_header) {

--- a/src/Tools/Code/code_runtime.ML	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Feb 29 23:09:06 2012 +0100
@@ -310,8 +310,9 @@
   | process_reflection (code, _) _ (SOME file_name) thy =
       let
         val preamble =
-          "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
-          ^ "; DO NOT EDIT! *)";
+          "(* Generated from " ^
+            Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
+          "; DO NOT EDIT! *)";
         val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
       in
         thy

--- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -60,10 +60,11 @@
 {
   /* header */
 
-  def node_header(): Exn.Result[Thy_Header] =
+  def node_header(): Document.Node_Header =
   {
     Swing_Thread.require()
-    Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
+    // FIXME assert(Isabelle.jedit_buffer(name.node) == Some(buffer))
+    Exn.capture { session.thy_load.check_thy(name) }
   }
 
 

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Feb 29 23:09:06 2012 +0100
@@ -52,7 +52,7 @@
     }
   }
 
-  override def check_thy(name: Document.Node.Name): Thy_Header =
+  override def read_header(name: Document.Node.Name): Thy_Header =
   {
     Swing_Thread.now {
       Isabelle.jedit_buffer(name.node) match {