# HG changeset patch
# User wenzelm
# Date 1361978864 -3600
# Node ID 0850d43cb355df7e57fd0d6ae0011058ef38634c
# Parent  05b1bbae748db11ce9b9b8023eb38f199d31fc08
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;

diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -83,7 +83,7 @@
 fun make_perspective command_ids : perspective =
   (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
 val no_perspective = make_perspective [];
 
 val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
@@ -102,9 +102,9 @@
 
 fun read_header node span =
   let
-    val (dir, {name = (name, _), imports, keywords, files}) = get_header node;
+    val (dir, {name = (name, _), imports, keywords}) = get_header node;
     val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
-  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end;
+  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective ids =
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -40,13 +40,12 @@
     sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
-      files: List[String],
       errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
     }
 
-    def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
+    def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
 
     object Name
     {
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -37,17 +37,14 @@
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
                     let
-                      val (master, (name, (imports, (keywords, (files, errors))))) =
+                      val (master, (name, (imports, (keywords, errors)))) =
                         pair string (pair string (pair (list string)
                           (pair (list (pair string
                             (option (pair (pair string (list string)) (list string)))))
-                            (pair (list string) (list string))))) a;
+                            (list string)))) a;
                       val imports' = map (rpair Position.none) imports;
-                      val (files', errors') =
-                        (map Path.explode files, errors)
-                          handle ERROR msg => ([], errors @ [msg]);
-                      val header = Thy_Header.make (name, Position.none) imports' keywords files';
-                    in Document.Deps (master, header, errors') end,
+                      val header = Thy_Header.make (name, Position.none) imports' keywords;
+                    in Document.Deps (master, header, errors) end,
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -289,14 +289,12 @@
               val dir = Isabelle_System.posix_path(name.dir)
               val imports = header.imports.map(_.node)
               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
-              // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
-              val files = header.files
               (Nil,
                 pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
                   pair(list(pair(Encode.string,
                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
-                  pair(list(Encode.string), list(Encode.string))))))(
-                (dir, (name.theory, (imports, (keywords, (files, header.errors))))))) },
+                  list(Encode.string)))))(
+                (dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -10,9 +10,8 @@
   type header =
    {name: string * Position.T,
     imports: (string * Position.T) list,
-    keywords: keywords,
-    files: Path.T list}
-  val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T list -> header
+    keywords: keywords}
+  val make: string * Position.T -> (string * Position.T) list -> keywords -> header
   val define_keywords: header -> unit
   val declare_keyword: string * Keyword.spec option -> theory -> theory
   val the_keyword: theory -> string -> Keyword.spec option
@@ -29,11 +28,10 @@
 type header =
  {name: string * Position.T,
   imports: (string * Position.T) list,
-  keywords: keywords,
-  files: Path.T list};
+  keywords: keywords};
 
-fun make name imports keywords files : header =
-  {name = name, imports = imports, keywords = keywords, files = files};
+fun make name imports keywords : header =
+  {name = name, imports = imports, keywords = keywords};
 
 
 
@@ -111,7 +109,7 @@
   Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
   Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   Parse.$$$ beginN >>
-  (fn ((name, imports), keywords) => make name imports keywords []);
+  (fn ((name, imports), keywords) => make name imports keywords);
 
 end;
 
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -12,8 +12,6 @@
 import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.util.matching.Regex
 
-import java.io.{File => JFile}
-
 
 object Thy_Header extends Parse.Parser
 {
@@ -72,7 +70,7 @@
       (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
-      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
+      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
 
     (keyword(HEADER) ~ tags) ~!
       ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -117,10 +115,9 @@
 sealed case class Thy_Header(
   name: String,
   imports: List[String],
-  keywords: Thy_Header.Keywords,
-  files: List[String])
+  keywords: Thy_Header.Keywords)
 {
   def map(f: String => String): Thy_Header =
-    Thy_Header(f(name), imports.map(f), keywords, files.map(f))
+    Thy_Header(f(name), imports.map(f), keywords)
 }
 
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -243,7 +243,7 @@
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
-    val header = Thy_Header.make (name, pos) imports keywords [];
+    val header = Thy_Header.make (name, pos) imports keywords;
 
     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
 
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -29,10 +29,15 @@
 
   sealed case class Dep(
     name: Document.Node.Name,
-    header0: Document.Node.Header,
-    future_header: JFuture[Exn.Result[Document.Node.Header]])
+    header: Document.Node.Header)
   {
-    def join_header: Document.Node.Header = Exn.release(future_header.get)
+    def load_files(syntax: Outer_Syntax): List[String] =
+    {
+      val string = thy_load.with_thy_text(name, _.toString)
+      if (thy_load.body_files_test(syntax, string))
+        thy_load.body_files(syntax, string)
+      else Nil
+    }
   }
 
   object Dependencies
@@ -46,24 +51,33 @@
     val seen: Set[Document.Node.Name])
   {
     def :: (dep: Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen)
+      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen)
 
     def + (name: Document.Node.Name): Dependencies =
       new Dependencies(rev_deps, keywords, seen = seen + name)
 
     def deps: List[Dep] = rev_deps.reverse
 
+    lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+
     def loaded_theories: Set[String] =
       (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
 
-    def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+    def load_files: List[Path] =
+    {
+      // FIXME par.map (!?)
+      ((Nil: List[Path]) /: rev_deps) {
+        case (files, dep) =>
+          dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a)) ::: files
+      }
+    }
   }
 
-  private def require_thys(files: Boolean, initiators: List[Document.Node.Name],
+  private def require_thys(initiators: List[Document.Node.Name],
       required: Dependencies, names: List[Document.Node.Name]): Dependencies =
-    (required /: names)(require_thy(files, initiators, _, _))
+    (required /: names)(require_thy(initiators, _, _))
 
-  private def require_thy(files: Boolean, initiators: List[Document.Node.Name],
+  private def require_thy(initiators: List[Document.Node.Name],
       required: Dependencies, name: Document.Node.Name): Dependencies =
   {
     if (required.seen(name)) required
@@ -75,46 +89,18 @@
 
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
-        val syntax = required.make_syntax
-
-        val header0 =
+        val header =
           try { thy_load.check_thy(name) }
           catch { case ERROR(msg) => err(msg) }
-
-        val future_header: JFuture[Exn.Result[Document.Node.Header]] =
-          if (files) {
-            val string = thy_load.with_thy_text(name, _.toString)
-            val syntax0 = syntax.add_keywords(header0.keywords)
-
-            if (thy_load.body_files_test(syntax0, string)) {
-              /* FIXME
-                  unstable in scala-2.9.2 on multicore hardware -- spurious NPE
-                  OK in scala-2.10.0.RC3 */
-              // default_thread_pool.submit(() =>
-                Library.future_value(Exn.capture {
-                  try {
-                    val files = thy_load.body_files(syntax0, string)
-                    header0.copy(files = header0.files ::: files)
-                  }
-                  catch { case ERROR(msg) => err(msg) }
-                })
-              //)
-            }
-            else Library.future_value(Exn.Res(header0))
-          }
-          else Library.future_value(Exn.Res(header0))
-
-        Dep(name, header0, future_header) ::
-          require_thys(files, name :: initiators, required + name, header0.imports)
+        Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
       }
       catch {
         case e: Throwable =>
-          val bad_header = Document.Node.bad_header(Exn.message(e))
-          Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name)
+          Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
       }
     }
   }
 
-  def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies =
-    require_thys(inlined_files, Nil, Dependencies.empty, names)
+  def dependencies(names: List[Document.Node.Name]): Dependencies =
+    require_thys(Nil, Dependencies.empty, names)
 }
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -132,7 +132,7 @@
     val master_file = check_file dir path;
     val text = File.read master_file;
 
-    val {name = (name, pos), imports, files = [], keywords} =
+    val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
     val _ = thy_name <> name andalso
       error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
@@ -207,7 +207,7 @@
 
 (* load_thy *)
 
-fun begin_theory master_dir {name, imports, keywords, files = []} parents =
+fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
   |> put_deps master_dir imports
   |> fold Thy_Header.declare_keyword keywords
@@ -238,7 +238,7 @@
   let
     val time = ! Toplevel.timing;
 
-    val {name = (name, _), files = [], ...} = header;
+    val {name = (name, _), ...} = header;
     val _ = Thy_Header.define_keywords header;
     val _ = Present.init_theory name;
     fun init () =
diff -r 05b1bbae748d -r 0850d43cb355 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -407,20 +407,18 @@
           }
 
           val thy_deps =
-            thy_info.dependencies(inlined_files,
+            thy_info.dependencies(
               info.theories.map(_._2).flatten.
                 map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = thy_deps.loaded_theories
-          val syntax = thy_deps.make_syntax
+          val syntax = thy_deps.syntax
+
+          val body_files = if (inlined_files) thy_deps.load_files else Nil
 
           val all_files =
-            (thy_deps.deps.map({ case dep =>
-              val thy = Path.explode(dep.name.node)
-              val files = dep.join_header.files.map(file =>
-                Path.explode(dep.name.dir) + Path.explode(file))
-              thy :: files
-            }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
+            (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+              info.files.map(file => info.dir + file)).map(_.expand)
 
           if (list_files)
             progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
@@ -432,7 +430,7 @@
                 error(msg + "\nThe error(s) above occurred in session " +
                   quote(name) + Position.here(info.pos))
             }
-          val errors = parent_errors ::: thy_deps.deps.map(dep => dep.join_header.errors).flatten
+          val errors = parent_errors
 
           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
       }))
diff -r 05b1bbae748d -r 0850d43cb355 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Feb 27 16:27:44 2013 +0100
@@ -157,7 +157,7 @@
 
         val thy_info = new Thy_Info(PIDE.thy_load)
         // FIXME avoid I/O in Swing thread!?!
-        val files = thy_info.dependencies(true, thys).deps.map(_.name.node).
+        val files = thy_info.dependencies(thys).deps.map(_.name.node).
           filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
         if (!files.isEmpty) {