36 else s + "(required by " + show_path(initiators.reverse) + ")" |
36 else s + "(required by " + show_path(initiators.reverse) + ")" |
37 |
37 |
38 |
38 |
39 /* dependencies */ |
39 /* dependencies */ |
40 |
40 |
41 type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header) |
41 type Deps = Map[String, Document.Node_Header] |
42 |
42 |
43 private def require_thys(ignored: String => Boolean, |
43 private def require_thys(initiators: List[String], |
44 initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps = |
44 deps: Deps, thys: List[(String, String)]): Deps = |
45 (deps /: strs)(require_thy(ignored, initiators, dir, _, _)) |
45 (deps /: thys)(require_thy(initiators, _, _)) |
46 |
46 |
47 private def require_thy(ignored: String => Boolean, |
47 private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps = |
48 initiators: List[String], dir: Path, deps: Deps, str: String): Deps = |
|
49 { |
48 { |
|
49 val (dir, str) = thy |
50 val path = Path.explode(str) |
50 val path = Path.explode(str) |
51 val name = path.base.implode |
51 val thy_name = path.base.implode |
|
52 val node_name = thy_load.append(dir, Thy_Header.thy_path(path)) |
52 |
53 |
53 if (deps.isDefinedAt(name) || ignored(name)) deps |
54 if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps |
54 else { |
55 else { |
55 val dir1 = dir + path.dir |
56 val dir1 = thy_load.append(dir, path.dir) |
56 try { |
57 try { |
57 if (initiators.contains(name)) error(cycle_msg(initiators)) |
58 if (initiators.contains(node_name)) error(cycle_msg(initiators)) |
58 val (text, header) = |
59 val header = |
59 try { thy_load.check_thy(dir1, name) } |
60 try { thy_load.check_thy(node_name) } |
60 catch { |
61 catch { |
61 case ERROR(msg) => |
62 case ERROR(msg) => |
62 cat_error(msg, "The error(s) above occurred while examining theory " + |
63 cat_error(msg, "The error(s) above occurred while examining theory file " + |
63 quote(name) + required_by("\n", initiators)) |
64 quote(node_name) + required_by("\n", initiators)) |
64 } |
65 } |
65 require_thys(ignored, name :: initiators, dir1, |
66 val thys = header.imports.map(str => (dir1, str)) |
66 deps + (name -> Exn.Res(text, header)), header.imports) |
67 require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys) |
67 } |
68 } |
68 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } |
69 catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) } |
69 } |
70 } |
70 } |
71 } |
71 |
72 |
72 def dependencies(dir: Path, str: String): Deps = |
73 def dependencies(thys: List[(String, String)]): Deps = |
73 require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str) |
74 require_thys(Nil, Map.empty, thys) |
74 } |
75 } |