--- a/src/Pure/PIDE/batch_session.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Pure/PIDE/batch_session.scala Wed Mar 15 10:31:42 2017 +0100
@@ -28,7 +28,7 @@
dirs = dirs, sessions = List(parent_session)).ok)
new RuntimeException
- val deps = Build.dependencies(verbose = verbose, tree = session_tree)
+ val deps = Sessions.dependencies(verbose = verbose, tree = session_tree)
val resources = new Resources(deps(parent_session))
val progress = new Console_Progress(verbose = verbose)
--- a/src/Pure/Thy/sessions.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Mar 15 10:31:42 2017 +0100
@@ -29,7 +29,7 @@
}
- /* base info */
+ /* base info and source dependencies */
object Base
{
@@ -47,8 +47,117 @@
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+ sealed case class Deps(deps: Map[String, Base])
+ {
+ def is_empty: Boolean = deps.isEmpty
+ def apply(name: String): Base = deps(name)
+ def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
+ }
- /* info */
+ def dependencies(
+ progress: Progress = No_Progress,
+ inlined_files: Boolean = false,
+ verbose: Boolean = false,
+ list_files: Boolean = false,
+ check_keywords: Set[String] = Set.empty,
+ tree: Tree): Deps =
+ Deps((Map.empty[String, Base] /: tree.topological_order)(
+ { case (deps, (name, info)) =>
+ if (progress.stopped) throw Exn.Interrupt()
+
+ try {
+ val resources =
+ new Resources(
+ info.parent match {
+ case None => Base.bootstrap
+ case Some(parent) => deps(parent)
+ })
+
+ if (verbose || list_files) {
+ val groups =
+ if (info.groups.isEmpty) ""
+ else info.groups.mkString(" (", " ", ")")
+ progress.echo("Session " + info.chapter + "/" + name + groups)
+ }
+
+ val thy_deps =
+ {
+ val root_theories =
+ info.theories.flatMap({
+ case (global, _, thys) =>
+ thys.map(thy =>
+ (resources.node_name(
+ if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
+ })
+ val thy_deps = resources.thy_info.dependencies(name, root_theories)
+
+ thy_deps.errors match {
+ case Nil => thy_deps
+ case errs => error(cat_lines(errs))
+ }
+ }
+
+ val known_theories =
+ (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+ val name = dep.name
+ known.get(name.theory) match {
+ case Some(name1) if name != name1 =>
+ error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
+ case _ =>
+ known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
+ }
+ })
+
+ val loaded_theories = thy_deps.loaded_theories
+ val keywords = thy_deps.keywords
+ val syntax = thy_deps.syntax
+
+ val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
+ val loaded_files =
+ if (inlined_files) {
+ val pure_files =
+ if (pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
+ else Nil
+ pure_files ::: thy_deps.loaded_files
+ }
+ else Nil
+
+ val all_files =
+ (theory_files ::: loaded_files :::
+ info.files.map(file => info.dir + file) :::
+ info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
+
+ if (list_files)
+ progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+
+ if (check_keywords.nonEmpty)
+ Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+
+ val sources = all_files.map(p => (p, SHA1.digest(p.file)))
+
+ val session_graph =
+ Present.session_graph(info.parent getOrElse "",
+ resources.base.loaded_theories, thy_deps.deps)
+
+ val base =
+ Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
+ deps + (name -> base)
+ }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg, "The error(s) above occurred in session " +
+ quote(name) + Position.here(info.pos))
+ }
+ }))
+
+ def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
+ {
+ val (_, tree) = load(options, dirs = dirs).selection(sessions = List(session))
+ dependencies(tree = tree)(session)
+ }
+
+
+ /* session tree */
sealed case class Info(
chapter: String,
@@ -67,9 +176,6 @@
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
}
-
- /* session tree */
-
object Tree
{
def apply(infos: Seq[(String, Info)]): Tree =
--- a/src/Pure/Tools/build.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 15 10:31:42 2017 +0100
@@ -93,119 +93,6 @@
}
- /* source dependencies and static content */
-
- sealed case class Deps(deps: Map[String, Sessions.Base])
- {
- def is_empty: Boolean = deps.isEmpty
- def apply(name: String): Sessions.Base = deps(name)
- def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
- }
-
- def dependencies(
- progress: Progress = No_Progress,
- inlined_files: Boolean = false,
- verbose: Boolean = false,
- list_files: Boolean = false,
- check_keywords: Set[String] = Set.empty,
- tree: Sessions.Tree): Deps =
- Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
- { case (deps, (name, info)) =>
- if (progress.stopped) throw Exn.Interrupt()
-
- try {
- val resources =
- new Resources(
- info.parent match {
- case None => Sessions.Base.bootstrap
- case Some(parent) => deps(parent)
- })
-
- if (verbose || list_files) {
- val groups =
- if (info.groups.isEmpty) ""
- else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + info.chapter + "/" + name + groups)
- }
-
- val thy_deps =
- {
- val root_theories =
- info.theories.flatMap({
- case (global, _, thys) =>
- thys.map(thy =>
- (resources.node_name(
- if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
- })
- val thy_deps = resources.thy_info.dependencies(name, root_theories)
-
- thy_deps.errors match {
- case Nil => thy_deps
- case errs => error(cat_lines(errs))
- }
- }
-
- val known_theories =
- (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
- val name = dep.name
- known.get(name.theory) match {
- case Some(name1) if name != name1 =>
- error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
- case _ =>
- known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
- }
- })
-
- val loaded_theories = thy_deps.loaded_theories
- val keywords = thy_deps.keywords
- val syntax = thy_deps.syntax
-
- val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
- val loaded_files =
- if (inlined_files) {
- val pure_files =
- if (Sessions.pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
- else Nil
- pure_files ::: thy_deps.loaded_files
- }
- else Nil
-
- val all_files =
- (theory_files ::: loaded_files :::
- info.files.map(file => info.dir + file) :::
- info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
-
- if (list_files)
- progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
-
- if (check_keywords.nonEmpty)
- Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
-
- val sources = all_files.map(p => (p, SHA1.digest(p.file)))
-
- val session_graph =
- Present.session_graph(info.parent getOrElse "",
- resources.base.loaded_theories, thy_deps.deps)
-
- val base =
- Sessions.Base(
- loaded_theories, known_theories, keywords, syntax, sources, session_graph)
- deps + (name -> base)
- }
- catch {
- case ERROR(msg) =>
- cat_error(msg, "The error(s) above occurred in session " +
- quote(name) + Position.here(info.pos))
- }
- }))
-
- def session_base(options: Options, session: String, dirs: List[Path] = Nil): Sessions.Base =
- {
- val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = List(session))
- dependencies(tree = tree)(session)
- }
-
-
/* jobs */
private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
@@ -431,7 +318,8 @@
val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
val full_tree = Sessions.load(build_options, dirs, select_dirs)
val (selected, selected_tree) = selection(full_tree)
- val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
+ val deps =
+ Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
def session_sources_stamp(name: String): String =
sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))
--- a/src/Tools/VSCode/src/build_vscode.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Wed Mar 15 10:31:42 2017 +0100
@@ -49,7 +49,7 @@
def build_grammar(options: Options, progress: Progress = No_Progress)
{
val logic = Grammar.default_logic
- val keywords = Build.session_base(options, logic).syntax.keywords
+ val keywords = Sessions.session_base(options, logic).syntax.keywords
val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
progress.echo(output_path.implode)
--- a/src/Tools/VSCode/src/grammar.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Wed Mar 15 10:31:42 2017 +0100
@@ -159,7 +159,7 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val keywords = Build.session_base(Options.init(), logic, dirs).syntax.keywords
+ val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
val output_path = output getOrElse Path.explode(default_output(logic))
Output.writeln(output_path.implode)
--- a/src/Tools/VSCode/src/server.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Wed Mar 15 10:31:42 2017 +0100
@@ -225,7 +225,7 @@
}
}
- val base = Build.session_base(options, session_name, session_dirs)
+ val base = Sessions.session_base(options, session_name, session_dirs)
val resources = new VSCode_Resources(options, base, log)
{
override def commit(change: Session.Change): Unit =
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Mar 15 10:08:27 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Mar 15 10:31:42 2017 +0100
@@ -82,7 +82,7 @@
def session_base(): Sessions.Base =
{
val base =
- try { Build.session_base(PIDE.options.value, session_name(), session_dirs()) }
+ try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
catch { case ERROR(_) => Sessions.Base.empty }
base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
}