# HG changeset patch
# User wenzelm
# Date 1346700634 -7200
# Node ID 673e0ed547afbd4e4f5afb4c0ef8d288aad2c552
# Parent  4e5e48c589eabfbd2c2b66a9dd542336cdfa981d
bypass slow check for inlined files, where it is not really required;

diff -r 4e5e48c589ea -r 673e0ed547af src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Sep 03 20:57:51 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Sep 03 21:30:34 2012 +0200
@@ -331,7 +331,8 @@
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
-  def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+  def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
+      tree: Session_Tree): Deps =
     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
           val (preloaded, parent_syntax, parent_errors) =
@@ -352,7 +353,7 @@
           }
 
           val thy_deps =
-            thy_info.dependencies(
+            thy_info.dependencies(inlined_files,
               info.theories.map(_._2).flatten.
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
@@ -381,15 +382,15 @@
           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
       }))
 
-  def session_content(dirs: List[Path], session: String): Session_Content =
+  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   {
     val (_, tree) =
       find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
-    dependencies(false, false, tree)(session)
+    dependencies(inlined_files, false, false, tree)(session)
   }
 
   def outer_syntax(session: String): Outer_Syntax =
-    session_content(Nil, session).check_errors.syntax
+    session_content(false, Nil, session).check_errors.syntax
 
 
   /* jobs */
@@ -548,7 +549,7 @@
     val options = (Options.init() /: build_options)(_ + _)
     val (descendants, tree) =
       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
-    val deps = dependencies(verbose, list_files, tree)
+    val deps = dependencies(true, verbose, list_files, tree)
     val queue = Queue(tree)
 
     def make_stamp(name: String): String =
diff -r 4e5e48c589ea -r 673e0ed547af src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Sep 03 20:57:51 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Sep 03 21:30:34 2012 +0200
@@ -50,11 +50,11 @@
     def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
 
-  private def require_thys(initiators: List[Document.Node.Name],
+  private def require_thys(files: Boolean, initiators: List[Document.Node.Name],
       required: Dependencies, names: List[Document.Node.Name]): Dependencies =
-    (required /: names)(require_thy(initiators, _, _))
+    (required /: names)(require_thy(files, initiators, _, _))
 
-  private def require_thy(initiators: List[Document.Node.Name],
+  private def require_thy(files: Boolean, initiators: List[Document.Node.Name],
       required: Dependencies, name: Document.Node.Name): Dependencies =
   {
     if (required.seen(name)) required
@@ -64,13 +64,16 @@
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val syntax = required.make_syntax
         val header =
-          try { thy_load.check_thy_files(syntax, name) }
+          try {
+            if (files) thy_load.check_thy_files(syntax, name)
+            else 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))
           }
-        (name, header) :: require_thys(name :: initiators, required + name, header.imports)
+        (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
       }
       catch {
         case e: Throwable =>
@@ -79,6 +82,6 @@
     }
   }
 
-  def dependencies(names: List[Document.Node.Name]): Dependencies =
-    require_thys(Nil, Dependencies.empty, names)
+  def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies =
+    require_thys(inlined_files, Nil, Dependencies.empty, names)
 }
diff -r 4e5e48c589ea -r 673e0ed547af src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 20:57:51 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 21:30:34 2012 +0200
@@ -316,11 +316,11 @@
     modes ::: List(logic)
   }
 
-  def session_content(): Build.Session_Content =
+  def session_content(inlined_files: Boolean): Build.Session_Content =
   {
     val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
     val name = Path.explode(session_args().last).base.implode  // FIXME more robust
-    Build.session_content(dirs, name).check_errors
+    Build.session_content(inlined_files, dirs, name).check_errors
   }
 
 
@@ -373,7 +373,7 @@
 
         val thy_info = new Thy_Info(Isabelle.thy_load)
         // FIXME avoid I/O in Swing thread!?!
-        val files = thy_info.dependencies(thys).deps.map(_._1.node).
+        val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
           filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
         if (!files.isEmpty) {
@@ -478,7 +478,7 @@
     Isabelle_System.init()
     Isabelle_System.install_fonts()
 
-    val content = Isabelle.session_content()
+    val content = Isabelle.session_content(false)
     val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
     Isabelle.session = new Session(thy_load)