# HG changeset patch # User wenzelm # Date 1392385184 -3600 # Node ID 60c159d490a210430d1436ac9b75dd2fcb941d29 # Parent e2cf2df4fd83bf1c357011f3fb63193ac67dd605 more integrity checks of theory names vs. full node names; diff -r e2cf2df4fd83 -r 60c159d490a2 src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala Fri Feb 14 11:10:28 2014 +0100 +++ b/src/Pure/General/multi_map.scala Fri Feb 14 14:39:44 2014 +0100 @@ -25,6 +25,8 @@ { /* Multi_Map operations */ + def iterator_list: Iterator[(A, List[B])] = rep.iterator + def get_list(a: A): List[B] = rep.getOrElse(a, Nil) def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = diff -r e2cf2df4fd83 -r 60c159d490a2 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Feb 14 11:10:28 2014 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Feb 14 14:39:44 2014 +0100 @@ -324,8 +324,8 @@ else error (loader_msg "incoherent imports for theory" [name] ^ Position.here require_pos ^ ":\n" ^ - Path.print node_name ^ " versus\n" ^ - Path.print node_name') + " " ^ Path.print node_name ^ "\n" ^ + " " ^ Path.print node_name') | check_entry _ = (); in (case try (String_Graph.get_node tasks) name of diff -r e2cf2df4fd83 -r 60c159d490a2 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Fri Feb 14 11:10:28 2014 +0100 +++ b/src/Pure/Thy/thy_info.scala Fri Feb 14 14:39:44 2014 +0100 @@ -42,23 +42,45 @@ object Dependencies { - val empty = new Dependencies(Nil, Nil, Set.empty) + val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty) } final class Dependencies private( rev_deps: List[Dep], val keywords: Thy_Header.Keywords, - val seen: Set[Document.Node.Name]) + val seen_names: Multi_Map[String, Document.Node.Name], + val seen_positions: Multi_Map[String, Position.T]) { def :: (dep: Dep): Dependencies = - new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen) + new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, + seen_names, seen_positions) - def + (name: Document.Node.Name): Dependencies = - new Dependencies(rev_deps, keywords, seen = seen + name) + def + (thy: (Document.Node.Name, Position.T)): Dependencies = + { + val (name, pos) = thy + new Dependencies(rev_deps, keywords, + seen_names + (name.theory -> name), + seen_positions + (name.theory -> pos)) + } def deps: List[Dep] = rev_deps.reverse - def errors: List[String] = deps.flatMap(dep => dep.header.errors) + def errors: List[String] = + { + val header_errors = deps.flatMap(dep => dep.header.errors) + val import_errors = + (for { + (theory, names) <- seen_names.iterator_list + if !thy_load.loaded_theories(theory) + if names.length > 1 + } yield + "Incoherent imports for theory " + quote(theory) + ":\n" + + cat_lines(names.flatMap(name => + seen_positions.get_list(theory).map(pos => + " " + quote(name.node) + Position.here(pos)))) + ).toList + header_errors ::: import_errors + } lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) @@ -79,32 +101,38 @@ } private def require_thys(initiators: List[Document.Node.Name], - required: Dependencies, names: List[Document.Node.Name]): Dependencies = - (required /: names)(require_thy(initiators, _, _)) + required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies = + (required /: thys)(require_thy(initiators, _, _)) private def require_thy(initiators: List[Document.Node.Name], - required: Dependencies, name: Document.Node.Name): Dependencies = + required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies = { - if (required.seen(name)) required - else if (thy_load.loaded_theories(name.theory)) required + name + val (name, require_pos) = thy + val theory = name.theory + + def message: String = + "The error(s) above occurred for theory " + quote(theory) + + required_by(initiators) + Position.here(require_pos) + + val required1 = required + thy + if (required.seen_names.isDefinedAt(theory) || thy_load.loaded_theories(theory)) + required1 else { - def message: String = - "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators) - try { if (initiators.contains(name)) error(cycle_msg(initiators)) val header = 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) + val imports = header.imports.map((_, Position.File(name.node))) + Dep(name, header) :: require_thys(name :: initiators, required1, imports) } catch { case e: Throwable => - Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name) + Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1 } } } - def dependencies(names: List[Document.Node.Name]): Dependencies = - require_thys(Nil, Dependencies.empty, names) + def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = + require_thys(Nil, Dependencies.empty, thys) } diff -r e2cf2df4fd83 -r 60c159d490a2 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Feb 14 11:10:28 2014 +0100 +++ b/src/Pure/Tools/build.scala Fri Feb 14 14:39:44 2014 +0100 @@ -432,7 +432,7 @@ val thy_deps = thy_info.dependencies( info.theories.map(_._2).flatten. - map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy)))) + map(thy => (thy_load.node_name(info.dir + Thy_Load.thy_path(thy)), info.pos))) thy_deps.errors match { case Nil =>