equal
deleted
inserted
replaced
10 class Thy_Info(thy_load: Thy_Load) |
10 class Thy_Info(thy_load: Thy_Load) |
11 { |
11 { |
12 /* messages */ |
12 /* messages */ |
13 |
13 |
14 private def show_path(names: List[String]): String = |
14 private def show_path(names: List[String]): String = |
15 names.map(Library.quote).mkString(" via ") |
15 names.map(quote).mkString(" via ") |
16 |
16 |
17 private def cycle_msg(names: List[String]): String = |
17 private def cycle_msg(names: List[String]): String = |
18 "Cyclic dependency of " + show_path(names) |
18 "Cyclic dependency of " + show_path(names) |
19 |
19 |
20 private def required_by(s: String, initiators: List[String]): String = |
20 private def required_by(s: String, initiators: List[String]): String = |
43 val (text, header) = |
43 val (text, header) = |
44 try { thy_load.check_thy(dir1, name) } |
44 try { thy_load.check_thy(dir1, name) } |
45 catch { |
45 catch { |
46 case ERROR(msg) => |
46 case ERROR(msg) => |
47 cat_error(msg, "The error(s) above occurred while examining theory " + |
47 cat_error(msg, "The error(s) above occurred while examining theory " + |
48 Library.quote(name) + required_by("\n", initiators)) |
48 quote(name) + required_by("\n", initiators)) |
49 } |
49 } |
50 require_thys(name :: initiators, dir1, |
50 require_thys(name :: initiators, dir1, |
51 deps + (name -> Exn.Res(text, header)), header.imports) |
51 deps + (name -> Exn.Res(text, header)), header.imports) |
52 } |
52 } |
53 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } |
53 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } |