bypass slow check for inlined files, where it is not really required;
authorwenzelm
Mon Sep 03 21:30:34 2012 +0200 (2012-09-03)
changeset 49098673e0ed547af
parent 49097 4e5e48c589ea
child 49099 10e899bb6530
bypass slow check for inlined files, where it is not really required;
src/Pure/System/build.scala
src/Pure/Thy/thy_info.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/System/build.scala	Mon Sep 03 20:57:51 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Mon Sep 03 21:30:34 2012 +0200
     1.3 @@ -331,7 +331,8 @@
     1.4      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
     1.5    }
     1.6  
     1.7 -  def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     1.8 +  def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
     1.9 +      tree: Session_Tree): Deps =
    1.10      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    1.11        { case (deps, (name, info)) =>
    1.12            val (preloaded, parent_syntax, parent_errors) =
    1.13 @@ -352,7 +353,7 @@
    1.14            }
    1.15  
    1.16            val thy_deps =
    1.17 -            thy_info.dependencies(
    1.18 +            thy_info.dependencies(inlined_files,
    1.19                info.theories.map(_._2).flatten.
    1.20                  map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
    1.21  
    1.22 @@ -381,15 +382,15 @@
    1.23            deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
    1.24        }))
    1.25  
    1.26 -  def session_content(dirs: List[Path], session: String): Session_Content =
    1.27 +  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
    1.28    {
    1.29      val (_, tree) =
    1.30        find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
    1.31 -    dependencies(false, false, tree)(session)
    1.32 +    dependencies(inlined_files, false, false, tree)(session)
    1.33    }
    1.34  
    1.35    def outer_syntax(session: String): Outer_Syntax =
    1.36 -    session_content(Nil, session).check_errors.syntax
    1.37 +    session_content(false, Nil, session).check_errors.syntax
    1.38  
    1.39  
    1.40    /* jobs */
    1.41 @@ -548,7 +549,7 @@
    1.42      val options = (Options.init() /: build_options)(_ + _)
    1.43      val (descendants, tree) =
    1.44        find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
    1.45 -    val deps = dependencies(verbose, list_files, tree)
    1.46 +    val deps = dependencies(true, verbose, list_files, tree)
    1.47      val queue = Queue(tree)
    1.48  
    1.49      def make_stamp(name: String): String =
     2.1 --- a/src/Pure/Thy/thy_info.scala	Mon Sep 03 20:57:51 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Sep 03 21:30:34 2012 +0200
     2.3 @@ -50,11 +50,11 @@
     2.4      def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
     2.5    }
     2.6  
     2.7 -  private def require_thys(initiators: List[Document.Node.Name],
     2.8 +  private def require_thys(files: Boolean, initiators: List[Document.Node.Name],
     2.9        required: Dependencies, names: List[Document.Node.Name]): Dependencies =
    2.10 -    (required /: names)(require_thy(initiators, _, _))
    2.11 +    (required /: names)(require_thy(files, initiators, _, _))
    2.12  
    2.13 -  private def require_thy(initiators: List[Document.Node.Name],
    2.14 +  private def require_thy(files: Boolean, initiators: List[Document.Node.Name],
    2.15        required: Dependencies, name: Document.Node.Name): Dependencies =
    2.16    {
    2.17      if (required.seen(name)) required
    2.18 @@ -64,13 +64,16 @@
    2.19          if (initiators.contains(name)) error(cycle_msg(initiators))
    2.20          val syntax = required.make_syntax
    2.21          val header =
    2.22 -          try { thy_load.check_thy_files(syntax, name) }
    2.23 +          try {
    2.24 +            if (files) thy_load.check_thy_files(syntax, name)
    2.25 +            else thy_load.check_thy(name)
    2.26 +          }
    2.27            catch {
    2.28              case ERROR(msg) =>
    2.29                cat_error(msg, "The error(s) above occurred while examining theory " +
    2.30                  quote(name.theory) + required_by(initiators))
    2.31            }
    2.32 -        (name, header) :: require_thys(name :: initiators, required + name, header.imports)
    2.33 +        (name, header) :: require_thys(files, name :: initiators, required + name, header.imports)
    2.34        }
    2.35        catch {
    2.36          case e: Throwable =>
    2.37 @@ -79,6 +82,6 @@
    2.38      }
    2.39    }
    2.40  
    2.41 -  def dependencies(names: List[Document.Node.Name]): Dependencies =
    2.42 -    require_thys(Nil, Dependencies.empty, names)
    2.43 +  def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies =
    2.44 +    require_thys(inlined_files, Nil, Dependencies.empty, names)
    2.45  }
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 20:57:51 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 21:30:34 2012 +0200
     3.3 @@ -316,11 +316,11 @@
     3.4      modes ::: List(logic)
     3.5    }
     3.6  
     3.7 -  def session_content(): Build.Session_Content =
     3.8 +  def session_content(inlined_files: Boolean): Build.Session_Content =
     3.9    {
    3.10      val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    3.11      val name = Path.explode(session_args().last).base.implode  // FIXME more robust
    3.12 -    Build.session_content(dirs, name).check_errors
    3.13 +    Build.session_content(inlined_files, dirs, name).check_errors
    3.14    }
    3.15  
    3.16  
    3.17 @@ -373,7 +373,7 @@
    3.18  
    3.19          val thy_info = new Thy_Info(Isabelle.thy_load)
    3.20          // FIXME avoid I/O in Swing thread!?!
    3.21 -        val files = thy_info.dependencies(thys).deps.map(_._1.node).
    3.22 +        val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
    3.23            filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
    3.24  
    3.25          if (!files.isEmpty) {
    3.26 @@ -478,7 +478,7 @@
    3.27      Isabelle_System.init()
    3.28      Isabelle_System.install_fonts()
    3.29  
    3.30 -    val content = Isabelle.session_content()
    3.31 +    val content = Isabelle.session_content(false)
    3.32      val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
    3.33      Isabelle.session = new Session(thy_load)
    3.34