# HG changeset patch # User wenzelm # Date 1489570302 -3600 # Node ID 4b0a43afc3fb6275766c8cf22e78b2071196f996 # Parent 13a6c81534a85eab6bf0282cc42c9ae17b5a94a7 clarified modules; diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Pure/PIDE/batch_session.scala --- 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) diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Pure/Thy/sessions.scala --- 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 = diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Pure/Tools/build.scala --- 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)) diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Tools/VSCode/src/build_vscode.scala --- 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) diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Tools/VSCode/src/grammar.scala --- 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) diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Tools/VSCode/src/server.scala --- 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 = diff -r 13a6c81534a8 -r 4b0a43afc3fb src/Tools/jEdit/src/jedit_sessions.scala --- 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(_)))) }