--- a/Admin/jenkins/build/ci_build_benchmark.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala Fri Apr 07 21:07:07 2017 +0200
@@ -12,7 +12,6 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(sessions: Sessions.T) =
- sessions.selection(session_groups = List("timing"))
+ def selection = Sessions.Selection(session_groups = List("timing"))
}
--- a/Admin/jenkins/build/ci_build_makeall.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala Fri Apr 07 21:07:07 2017 +0200
@@ -11,7 +11,6 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(sessions: Sessions.T) =
- sessions.selection(all_sessions = true)
+ def selection = Sessions.Selection(all_sessions = true)
}
--- a/Admin/jenkins/build/ci_build_makeall_seq.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall_seq.scala Fri Apr 07 21:07:07 2017 +0200
@@ -11,7 +11,6 @@
def pre_hook(args: List[String]) = {}
def post_hook(results: Build.Results) = {}
- def select_sessions(sessions: Sessions.T) =
- sessions.selection(all_sessions = true)
+ def selection = Sessions.Selection(all_sessions = true)
}
--- a/src/Pure/Admin/build_doc.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Admin/build_doc.scala Fri Apr 07 21:07:07 2017 +0200
@@ -24,7 +24,7 @@
{
val selection =
for {
- (name, info) <- Sessions.load(options).topological_order
+ (name, info) <- Sessions.load(options).build_topological_order
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
--- a/src/Pure/Admin/ci_profile.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Admin/ci_profile.scala Fri Apr 07 21:07:07 2017 +0200
@@ -19,7 +19,7 @@
val progress = new Console_Progress(verbose = true)
val start_time = Time.now()
val results = progress.interrupt_handler {
- Build.build_selection(
+ Build.build(
options = options,
progress = progress,
clean_build = clean,
@@ -28,7 +28,7 @@
dirs = include,
select_dirs = select,
system_mode = true,
- selection = select_sessions _)
+ selection = selection)
}
val end_time = Time.now()
(results, end_time - start_time)
@@ -146,5 +146,5 @@
def pre_hook(args: List[String]): Unit
def post_hook(results: Build.Results): Unit
- def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
+ def selection: Sessions.Selection
}
--- a/src/Pure/ML/ml_syntax.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/ML/ml_syntax.scala Fri Apr 07 21:07:07 2017 +0200
@@ -46,6 +46,12 @@
quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+ /* pair */
+
+ def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
+ "(" + f(pair._1) + ", " + g(pair._2) + ")"
+
+
/* list */
def print_list[A](f: A => String)(list: List[A]): String =
--- a/src/Pure/PIDE/resources.ML Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Fri Apr 07 21:07:07 2017 +0200
@@ -6,6 +6,9 @@
signature RESOURCES =
sig
+ val set_session_base: {known_theories: (string * string) list} -> unit
+ val reset_session_base: unit -> unit
+ val known_theory: string -> Path.T option
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val thy_path: Path.T -> Path.T
@@ -25,6 +28,23 @@
structure Resources: RESOURCES =
struct
+(* session base *)
+
+val global_session_base =
+ Synchronized.var "Sessions.base"
+ ({known_theories = Symtab.empty: Path.T Symtab.table});
+
+fun set_session_base {known_theories} =
+ Synchronized.change global_session_base
+ (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+
+fun reset_session_base () =
+ set_session_base {known_theories = []};
+
+fun known_theory name =
+ Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+
+
(* manage source files *)
type files =
@@ -62,15 +82,20 @@
fun check_thy dir thy_name =
let
- val path = thy_path (Path.basic thy_name);
- val master_file = check_file dir path;
+ val thy_base_name = Long_Name.base_name thy_name;
+ val thy_path = thy_path (Path.basic thy_base_name);
+ val master_file =
+ (case known_theory thy_name of
+ NONE => check_file dir thy_path
+ | SOME known_path => check_file Path.current known_path);
val text = File.read master_file;
val {name = (name, pos), imports, keywords} =
Thy_Header.read (Path.position master_file) text;
- val _ = thy_name <> name andalso
- error ("Bad theory name " ^ quote name ^
- " for file " ^ Path.print path ^ Position.here pos);
+ val _ =
+ thy_base_name <> name andalso
+ error ("Bad theory name " ^ quote name ^
+ " for file " ^ Path.print thy_path ^ Position.here pos);
in
{master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
imports = imports, keywords = keywords}
--- a/src/Pure/PIDE/resources.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Fri Apr 07 21:07:07 2017 +0200
@@ -74,15 +74,14 @@
if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
else Long_Name.qualify(session_name, theory0)
- session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
- {
- case Some(name) if session_base.loaded_theory(name) => name.loaded_theory
- case Some(name) => name
- case None =>
- val path = Path.explode(s)
- val node = append(dir, thy_path(path))
- val master_dir = append(dir, path.dir)
- Document.Node.Name(node, master_dir, theory)
+ session_base.loaded_theories.get(theory) orElse
+ session_base.loaded_theories.get(theory0) orElse
+ session_base.known_theories.get(theory) orElse
+ session_base.known_theories.get(theory0) getOrElse {
+ val path = Path.explode(s)
+ val node = append(dir, thy_path(path))
+ val master_dir = append(dir, path.dir)
+ Document.Node.Name(node, master_dir, theory)
}
}
--- a/src/Pure/Thy/sessions.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Apr 07 21:07:07 2017 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/sessions.scala
Author: Makarius
-Isabelle session information.
+Cumulative session information.
*/
package isabelle
@@ -27,11 +27,28 @@
lazy val bootstrap: Base =
Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
+
+ private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name])
+ : Map[String, Document.Node.Name] =
+ {
+ val bases_iterator =
+ for { base <- bases.iterator; (_, name) <- base.known_theories.iterator }
+ yield name
+
+ (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({
+ case (known, 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)
+ }
+ })
+ }
}
sealed case class Base(
global_theories: Set[String] = Set.empty,
- loaded_theories: Set[String] = Set.empty,
+ loaded_theories: Map[String, Document.Node.Name] = Map.empty,
known_theories: Map[String, Document.Node.Name] = Map.empty,
keywords: Thy_Header.Keywords = Nil,
syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -39,7 +56,11 @@
session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
{
def loaded_theory(name: Document.Node.Name): Boolean =
- loaded_theories.contains(name.theory)
+ loaded_theories.isDefinedAt(name.theory)
+
+ def dest_known_theories: List[(String, String)] =
+ for ((theory, node_name) <- known_theories.toList)
+ yield (theory, node_name.node)
}
sealed case class Deps(sessions: Map[String, Base])
@@ -47,6 +68,9 @@
def is_empty: Boolean = sessions.isEmpty
def apply(name: String): Base = sessions(name)
def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
+
+ def all_known_theories: Map[String, Document.Node.Name] =
+ Base.known_theories(sessions.toList.map(_._2), Nil)
}
def deps(sessions: T,
@@ -57,8 +81,8 @@
check_keywords: Set[String] = Set.empty,
global_theories: Set[String] = Set.empty): Deps =
{
- Deps((Map.empty[String, Base] /: sessions.topological_order)({
- case (sessions, (name, info)) =>
+ Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
+ case (sessions, (session_name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
try {
@@ -67,13 +91,13 @@
case None => Base.bootstrap
case Some(parent) => sessions(parent)
}
- val resources = new Resources(name, parent_base)
+ val resources = new Resources(session_name, parent_base)
if (verbose || list_files) {
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + info.chapter + "/" + name + groups)
+ progress.echo("Session " + info.chapter + "/" + session_name + groups)
}
val thy_deps =
@@ -90,27 +114,13 @@
}
}
- val known_theories =
- (parent_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) // legacy
- }
- })
-
- 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 (is_pure(name)) {
+ if (is_pure(session_name)) {
val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
val files =
roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
@@ -135,29 +145,41 @@
val base =
Base(global_theories = global_theories,
- loaded_theories = loaded_theories,
- known_theories = known_theories,
- keywords = keywords,
+ loaded_theories = thy_deps.loaded_theories,
+ known_theories =
+ Base.known_theories(
+ parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)),
+ keywords = thy_deps.keywords,
syntax = syntax,
sources = all_files.map(p => (p, SHA1.digest(p.file))),
session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
- sessions + (name -> base)
+ sessions + (session_name -> base)
}
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred in session " +
- quote(name) + Position.here(info.pos))
+ quote(session_name) + Position.here(info.pos))
}
}))
}
- def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
+ def session_base(
+ options: Options,
+ session: String,
+ dirs: List[Path] = Nil,
+ all_known_theories: Boolean = false): Base =
{
val full_sessions = load(options, dirs = dirs)
- val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
+ val global_theories = full_sessions.global_theories
+ val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
- deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
+ if (all_known_theories) {
+ val deps = Sessions.deps(full_sessions, global_theories = global_theories)
+ deps(session).copy(known_theories = deps.all_known_theories)
+ }
+ else
+ deps(selected_sessions, global_theories = global_theories)(session)
}
@@ -172,6 +194,7 @@
parent: Option[String],
description: String,
options: Options,
+ imports: List[String],
theories: List[(Options, List[String])],
global_theories: List[String],
files: List[Path],
@@ -181,62 +204,32 @@
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
}
- def make(infos: Traversable[(String, Info)]): T =
+ object Selection
{
- val graph1 =
- (Graph.string[Info] /: infos) {
- case (graph, (name, info)) =>
- if (graph.defined(name))
- error("Duplicate session " + quote(name) + Position.here(info.pos) +
- Position.here(graph.get_node(name).pos))
- else graph.new_node(name, info)
- }
- val graph2 =
- (graph1 /: graph1.iterator) {
- case (graph, (name, (info, _))) =>
- info.parent match {
- case None => graph
- case Some(parent) =>
- if (!graph.defined(parent))
- error("Bad parent session " + quote(parent) + " for " +
- quote(name) + Position.here(info.pos))
-
- try { graph.add_edge_acyclic(parent, name) }
- catch {
- case exn: Graph.Cycles[_] =>
- error(cat_lines(exn.cycles.map(cycle =>
- "Cyclic session dependency of " +
- cycle.map(c => quote(c.toString)).mkString(" via "))) +
- Position.here(info.pos))
- }
- }
- }
-
- new T(graph2)
+ val empty: Selection = Selection()
}
- final class T private[Sessions](val graph: Graph[String, Info])
- extends PartialFunction[String, Info]
+ sealed case class Selection(
+ requirements: Boolean = false,
+ all_sessions: Boolean = false,
+ exclude_session_groups: List[String] = Nil,
+ exclude_sessions: List[String] = Nil,
+ session_groups: List[String] = Nil,
+ sessions: List[String] = Nil)
{
- def apply(name: String): Info = graph.get_node(name)
- def isDefinedAt(name: String): Boolean = graph.defined(name)
+ def + (other: Selection): Selection =
+ Selection(
+ requirements = requirements || other.requirements,
+ all_sessions = all_sessions || other.all_sessions,
+ exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
+ exclude_sessions = exclude_sessions ::: other.exclude_sessions,
+ session_groups = session_groups ::: other.session_groups,
+ sessions = sessions ::: other.sessions)
- def global_theories: Set[String] =
- (for {
- (_, (info, _)) <- graph.iterator
- name <- info.global_theories.iterator }
- yield name).toSet
-
- def selection(
- requirements: Boolean = false,
- all_sessions: Boolean = false,
- exclude_session_groups: List[String] = Nil,
- exclude_sessions: List[String] = Nil,
- session_groups: List[String] = Nil,
- sessions: List[String] = Nil): (List[String], T) =
+ def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
{
val bad_sessions =
- SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
+ SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
val excluded =
@@ -245,7 +238,7 @@
val exclude_group_sessions =
(for {
(name, (info, _)) <- graph.iterator
- if apply(name).groups.exists(exclude_group)
+ if graph.get_node(name).groups.exists(exclude_group)
} yield name).toList
graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
}
@@ -258,7 +251,7 @@
val select = sessions.toSet
(for {
(name, (info, _)) <- graph.iterator
- if info.select || select(name) || apply(name).groups.exists(select_group)
+ if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
} yield name).toList
}
}.filterNot(excluded)
@@ -267,17 +260,89 @@
if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
else pre_selected
- val graph1 = graph.restrict(graph.all_preds(selected).toSet)
- (selected, new T(graph1))
+ (selected, graph.restrict(graph.all_preds(selected).toSet))
+ }
+ }
+
+ def make(infos: Traversable[(String, Info)]): T =
+ {
+ def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
+ : Graph[String, Info] =
+ {
+ def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
+ {
+ if (!g.defined(parent))
+ error("Bad " + kind + " session " + quote(parent) + " for " +
+ quote(name) + Position.here(pos))
+
+ try { g.add_edge_acyclic(parent, name) }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic session dependency of " +
+ cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
+ }
+ }
+ (graph /: graph.iterator) {
+ case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
+ }
}
- def ancestors(name: String): List[String] =
- graph.all_preds(List(name)).tail.reverse
+ val graph0 =
+ (Graph.string[Info] /: infos) {
+ case (graph, (name, info)) =>
+ if (graph.defined(name))
+ error("Duplicate session " + quote(name) + Position.here(info.pos) +
+ Position.here(graph.get_node(name).pos))
+ else graph.new_node(name, info)
+ }
+ val graph1 = add_edges(graph0, "parent", _.parent)
+ val graph2 = add_edges(graph1, "imports", _.imports)
+
+ new T(graph1, graph2)
+ }
+
+ final class T private[Sessions](
+ val build_graph: Graph[String, Info],
+ val imports_graph: Graph[String, Info])
+ {
+ def apply(name: String): Info = imports_graph.get_node(name)
+ def get(name: String): Option[Info] =
+ if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
- def topological_order: List[(String, Info)] =
- graph.topological_order.map(name => (name, apply(name)))
+ def global_theories: Set[String] =
+ (Set.empty[String] /:
+ (for {
+ (_, (info, _)) <- imports_graph.iterator
+ thy <- info.global_theories.iterator }
+ yield (thy, info.pos)))(
+ { case (set, (thy, pos)) =>
+ if (set.contains(thy))
+ error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
+ else set + thy
+ })
- override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
+ def selection(select: Selection): (List[String], T) =
+ {
+ val (_, build_graph1) = select(build_graph)
+ val (selected, imports_graph1) = select(imports_graph)
+ (selected, new T(build_graph1, imports_graph1))
+ }
+
+ def build_ancestors(name: String): List[String] =
+ build_graph.all_preds(List(name)).tail.reverse
+
+ def build_descendants(names: List[String]): List[String] =
+ build_graph.all_succs(names)
+
+ def build_topological_order: List[(String, Info)] =
+ build_graph.topological_order.map(name => (name, apply(name)))
+
+ def imports_topological_order: List[(String, Info)] =
+ imports_graph.topological_order.map(name => (name, apply(name)))
+
+ override def toString: String =
+ imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
}
@@ -291,6 +356,7 @@
private val IN = "in"
private val DESCRIPTION = "description"
private val OPTIONS = "options"
+ private val SESSIONS = "sessions"
private val THEORIES = "theories"
private val GLOBAL = "global"
private val FILES = "files"
@@ -302,6 +368,7 @@
(SESSION, Keyword.THY_DECL) +
(DESCRIPTION, Keyword.QUASI_COMMAND) +
(OPTIONS, Keyword.QUASI_COMMAND) +
+ (SESSIONS, Keyword.QUASI_COMMAND) +
(THEORIES, Keyword.QUASI_COMMAND) +
(FILES, Keyword.QUASI_COMMAND) +
(DOCUMENT_FILES, Keyword.QUASI_COMMAND)
@@ -318,6 +385,7 @@
parent: Option[String],
description: String,
options: List[Options.Spec],
+ imports: List[String],
theories: List[(List[Options.Spec], List[(String, Boolean)])],
files: List[String],
document_files: List[(String, String)]) extends Entry
@@ -363,11 +431,12 @@
(opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
(($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
(($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$(SESSIONS) ~! rep(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~
rep1(theories) ~
(($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
(rep(document_files) ^^ (x => x.flatten))))) ^^
- { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
- Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
+ Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
}
def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
@@ -401,12 +470,12 @@
val meta_digest =
SHA1.digest((entry_chapter, name, entry.parent, entry.options,
- entry.theories, entry.files, entry.document_files).toString)
+ entry.imports, entry.theories, entry.files, entry.document_files).toString)
val info =
Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
- entry.parent, entry.description, session_options, theories, global_theories,
- files, document_files, meta_digest)
+ entry.parent, entry.description, session_options, entry.imports, theories,
+ global_theories, files, document_files, meta_digest)
(name, info)
}
--- a/src/Pure/Thy/thy_info.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Fri Apr 07 21:07:07 2017 +0200
@@ -67,7 +67,7 @@
val import_errors =
(for {
(theory, imports) <- seen_theory.iterator_list
- if !resources.session_base.loaded_theories(theory)
+ if !resources.session_base.loaded_theories.isDefinedAt(theory)
if imports.length > 1
} yield {
"Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -80,11 +80,12 @@
lazy val syntax: Outer_Syntax =
resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
- def loaded_theories: Set[String] =
+ def loaded_theories: Map[String, Document.Node.Name] =
(resources.session_base.loaded_theories /: rev_deps) {
case (loaded, dep) =>
- loaded + dep.name.theory +
- Long_Name.base_name(dep.name.theory) // legacy
+ val name = dep.name.loaded_theory
+ loaded + (name.theory -> name) +
+ (Long_Name.base_name(name.theory) -> name) // legacy
}
def loaded_files: List[Path] =
--- a/src/Pure/Tools/build.ML Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 07 21:07:07 2017 +0200
@@ -144,30 +144,37 @@
chapter: string,
name: string,
master_dir: Path.T,
- theories: (Options.T * (string * Position.T) list) list};
+ theories: (Options.T * (string * Position.T) list) list,
+ known_theories: (string * string) list};
fun decode_args yxml =
let
open XML.Decode;
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
- (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
+ (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
+ (theories, known_theories)))))))))))) =
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
(pair (list (pair string string)) (pair string (pair string (pair string (pair string
- (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
+ (pair string
+ (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
+ (list (pair string string)))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
verbose = verbose, browser_info = Path.explode browser_info,
document_files = map (apply2 Path.explode) document_files,
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
- name = name, master_dir = Path.explode master_dir, theories = theories}
+ name = name, master_dir = Path.explode master_dir, theories = theories,
+ known_theories = known_theories}
end;
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
- document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
+ document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
let
val symbols = HTML.make_symbols symbol_codes;
+ val _ = Resources.set_session_base {known_theories = known_theories};
+
val _ =
Session.init
symbols
@@ -191,6 +198,8 @@
|> session_timing name verbose
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
+
+ val _ = Resources.reset_session_base ();
val _ = Par_Exn.release_all [res1, res2];
in () end;
--- a/src/Pure/Tools/build.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 07 21:07:07 2017 +0200
@@ -65,7 +65,7 @@
def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
{
- val graph = sessions.graph
+ val graph = sessions.build_graph
val names = graph.keys
val timings = names.map(name => (name, load_timings(store, name)))
@@ -204,11 +204,13 @@
pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
- list(pair(Options.encode, list(string))))))))))))))(
+ pair(list(pair(Options.encode, list(string))),
+ list(pair(string, string))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name, (Path.current,
- info.theories))))))))))))
+ (info.theories,
+ deps(name).dest_known_theories)))))))))))))
})
val env =
@@ -351,51 +353,20 @@
exclude_session_groups: List[String] = Nil,
exclude_sessions: List[String] = Nil,
session_groups: List[String] = Nil,
- sessions: List[String] = Nil): Results =
- {
- build_selection(
- options = options,
- progress = progress,
- build_heap = build_heap,
- clean_build = clean_build,
- dirs = dirs,
- select_dirs = select_dirs,
- numa_shuffling = numa_shuffling,
- max_jobs = max_jobs,
- list_files = list_files,
- check_keywords = check_keywords,
- no_build = no_build,
- system_mode = system_mode,
- verbose = verbose,
- pide = pide,
- selection = { full_sessions =>
- full_sessions.selection(requirements, all_sessions,
- exclude_session_groups, exclude_sessions, session_groups, sessions) })
- }
-
- def build_selection(
- options: Options,
- progress: Progress = No_Progress,
- build_heap: Boolean = false,
- clean_build: Boolean = false,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- numa_shuffling: Boolean = false,
- max_jobs: Int = 1,
- list_files: Boolean = false,
- check_keywords: Set[String] = Set.empty,
- no_build: Boolean = false,
- system_mode: Boolean = false,
- verbose: Boolean = false,
- pide: Boolean = false,
- selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
- ): Results =
+ sessions: List[String] = Nil,
+ selection: Sessions.Selection = Sessions.Selection.empty): Results =
{
/* session selection and dependencies */
val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+
val full_sessions = Sessions.load(build_options, dirs, select_dirs)
- val (selected, selected_sessions) = selection(full_sessions)
+
+ val (selected, selected_sessions) =
+ full_sessions.selection(
+ Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+ exclude_sessions, session_groups, sessions) + selection)
+
val deps =
Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
verbose = verbose, list_files = list_files, check_keywords = check_keywords,
@@ -414,7 +385,7 @@
// optional cleanup
if (clean_build) {
- for (name <- full_sessions.graph.all_succs(selected)) {
+ for (name <- full_sessions.build_descendants(selected)) {
val files =
List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
map(store.output_dir + _).filter(_.is_file)
@@ -520,7 +491,7 @@
//{{{ check/start next job
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
- val ancestor_results = selected_sessions.ancestors(name).map(results(_))
+ val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
--- a/src/Pure/Tools/ml_console.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/ml_console.scala Fri Apr 07 21:07:07 2017 +0200
@@ -72,7 +72,10 @@
val process =
ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
- raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
+ raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+ session_base =
+ if (raw_ml_system) None
+ else Some(Sessions.session_base(options, logic, dirs)))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)
--- a/src/Pure/Tools/ml_process.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala Fri Apr 07 21:07:07 2017 +0200
@@ -24,15 +24,17 @@
cleanup: () => Unit = () => (),
channel: Option[System_Channel] = None,
sessions: Option[Sessions.T] = None,
+ session_base: Option[Sessions.Base] = None,
store: Sessions.Store = Sessions.store()): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
val heaps: List[String] =
if (raw_ml_system) Nil
else {
+ val selection = Sessions.Selection(sessions = List(logic_name))
val (_, selected_sessions) =
- sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
- (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
+ sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
+ (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
map(a => File.platform_path(store.heap(a)))
}
@@ -88,6 +90,18 @@
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
+ // session base
+ val eval_session_base =
+ session_base match {
+ case None => Nil
+ case Some(base) =>
+ List("Resources.set_session_base {known_theories = " +
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(
+ ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+ }
+
+ // process
val eval_process =
if (heaps.isEmpty)
List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
@@ -113,7 +127,7 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_process).
+ (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
map(eval => List("--eval", eval)).flatten ::: args
Bash.process(
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 07 21:07:07 2017 +0200
@@ -38,10 +38,10 @@
options.string(option_name))
(for {
- tree <-
+ sessions <-
try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
catch { case ERROR(_) => None }
- info <- tree.lift(logic)
+ info <- sessions.get(logic)
parent <- info.parent
if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
} yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
@@ -75,9 +75,9 @@
def session_list(options: Options): List[String] =
{
- val session_tree = Sessions.load(options, dirs = session_dirs())
+ val sessions = Sessions.load(options, dirs = session_dirs())
val (main_sessions, other_sessions) =
- session_tree.topological_order.partition(p => p._2.groups.contains("main"))
+ sessions.imports_topological_order.partition(p => p._2.groups.contains("main"))
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
}