--- a/src/Pure/PIDE/document.scala Thu Nov 21 13:43:42 2013 +0100
+++ b/src/Pure/PIDE/document.scala Thu Nov 21 19:13:49 2013 +0100
@@ -62,6 +62,9 @@
errors: List[String] = Nil)
{
def error(msg: String): Header = copy(errors = errors ::: List(msg))
+
+ def cat_errors(msg2: String): Header =
+ copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
}
def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
--- a/src/Pure/Thy/thy_info.scala Thu Nov 21 13:43:42 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala Thu Nov 21 19:13:49 2013 +0100
@@ -58,6 +58,8 @@
def deps: List[Dep] = rev_deps.reverse
+ def errors: List[String] = deps.flatMap(dep => dep.header.errors)
+
lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
def loaded_theories: Set[String] =
@@ -86,15 +88,15 @@
if (required.seen(name)) required
else if (thy_load.loaded_theories(name.theory)) required + name
else {
- def err(msg: String): Nothing =
- cat_error(msg, "The error(s) above occurred while examining theory " +
- quote(name.theory) + required_by(initiators))
+ def message: String =
+ "The error(s) above occurred while examining theory " +
+ quote(name.theory) + required_by(initiators)
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
val header =
- try { thy_load.check_thy(name) }
- catch { case ERROR(msg) => err(msg) }
+ try { thy_load.check_thy(name).cat_errors(message) }
+ catch { case ERROR(msg) => cat_error(msg, message) }
Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
}
catch {
--- a/src/Pure/Tools/build.scala Thu Nov 21 13:43:42 2013 +0100
+++ b/src/Pure/Tools/build.scala Thu Nov 21 19:13:49 2013 +0100
@@ -409,65 +409,68 @@
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) =
- info.parent match {
- case None =>
- (Set.empty[String], Outer_Syntax.init())
- case Some(parent_name) =>
- val parent = deps(parent_name)
- (parent.loaded_theories, parent.syntax)
- }
- val thy_load = new Thy_Load(preloaded, parent_syntax)
- val thy_info = new Thy_Info(thy_load)
+ try {
+ val (preloaded, parent_syntax) =
+ info.parent match {
+ case None =>
+ (Set.empty[String], Outer_Syntax.init())
+ case Some(parent_name) =>
+ val parent = deps(parent_name)
+ (parent.loaded_theories, parent.syntax)
+ }
+ val thy_load = new Thy_Load(preloaded, parent_syntax)
+ val thy_info = new Thy_Info(thy_load)
- if (verbose || list_files) {
- val groups =
- if (info.groups.isEmpty) ""
- else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + info.chapter + "/" + name + groups)
- }
+ if (verbose || list_files) {
+ val groups =
+ if (info.groups.isEmpty) ""
+ else info.groups.mkString(" (", " ", ")")
+ progress.echo("Session " + info.chapter + "/" + name + groups)
+ }
- val thy_deps =
- thy_info.dependencies(
- info.theories.map(_._2).flatten.
- map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
+ val thy_deps =
+ thy_info.dependencies(
+ info.theories.map(_._2).flatten.
+ map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
- val loaded_theories = thy_deps.loaded_theories
- val keywords = thy_deps.keywords
- val syntax = thy_deps.syntax
+ thy_deps.errors match {
+ case Nil =>
+ case errs => error(cat_lines(errs))
+ }
- val body_files = if (inlined_files) thy_deps.load_files else Nil
+ val loaded_theories = thy_deps.loaded_theories
+ val keywords = thy_deps.keywords
+ val syntax = thy_deps.syntax
- val all_files =
- (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
- info.files.map(file => info.dir + file)).map(_.expand)
+ val body_files = if (inlined_files) thy_deps.load_files else Nil
- if (list_files) {
- progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
- for {
- file <- all_files
- if file.split_ext._2 == "ML"
- } {
- val path = info.dir + file
- try { Symbol.decode_strict(File.read(path)) }
- catch {
- case ERROR(msg) =>
- cat_error(msg,
- "The error(s) above occurred in session " + quote(name) +
- " file " + path.toString)
+ val all_files =
+ (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+ info.files.map(file => info.dir + file)).map(_.expand)
+
+ if (list_files) {
+ progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+ for {
+ file <- all_files
+ if file.split_ext._2 == "ML"
+ } {
+ val path = info.dir + file
+ try { Symbol.decode_strict(File.read(path)) }
+ catch {
+ case ERROR(msg) => cat_error(msg, "The error(s) above occurred in file " + path)
+ }
}
}
- }
+
+ val sources = all_files.map(p => (p, SHA1.digest(p.file)))
- val sources =
- try { all_files.map(p => (p, SHA1.digest(p.file))) }
- catch {
- case ERROR(msg) =>
- error(msg + "\nThe error(s) above occurred in session " +
- quote(name) + Position.here(info.pos))
- }
-
- deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
+ deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
+ }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg, "The error(s) above occurred in session " +
+ quote(name) + Position.here(info.pos))
+ }
}))
def session_dependencies(
--- a/src/Pure/library.scala Thu Nov 21 13:43:42 2013 +0100
+++ b/src/Pure/library.scala Thu Nov 21 19:13:49 2013 +0100
@@ -26,9 +26,12 @@
def error(message: String): Nothing = throw ERROR(message)
+ def cat_message(msg1: String, msg2: String): String =
+ if (msg1 == "") msg2
+ else msg1 + "\n" + msg2
+
def cat_error(msg1: String, msg2: String): Nothing =
- if (msg1 == "") error(msg1)
- else error(msg1 + "\n" + msg2)
+ error(cat_message(msg1, msg2))
/* separated chunks */