# HG changeset patch # User wenzelm # Date 1385052623 -3600 # Node ID 2a3053472ec334bc6c2118845a2b5e4e93ef9517 # Parent 41e4ba92a9792c06d0ed87e4585133fb16e1dc4b actually expose errors of cumulative theory dependencies; more informative error messages; diff -r 41e4ba92a979 -r 2a3053472ec3 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Nov 21 17:45:37 2013 +0100 +++ b/src/Pure/PIDE/document.scala Thu Nov 21 17:50:23 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)) diff -r 41e4ba92a979 -r 2a3053472ec3 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Nov 21 17:45:37 2013 +0100 +++ b/src/Pure/Thy/thy_info.scala Thu Nov 21 17:50:23 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 { diff -r 41e4ba92a979 -r 2a3053472ec3 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Nov 21 17:45:37 2013 +0100 +++ b/src/Pure/Tools/build.scala Thu Nov 21 17:50:23 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(