23 |
23 |
24 class Thy_Info(thy_load: Thy_Load) |
24 class Thy_Info(thy_load: Thy_Load) |
25 { |
25 { |
26 /* messages */ |
26 /* messages */ |
27 |
27 |
28 private def show_path(names: List[String]): String = |
28 private def show_path(names: List[Document.Node.Name]): String = |
29 names.map(quote).mkString(" via ") |
29 names.map(name => quote(name.theory)).mkString(" via ") |
30 |
30 |
31 private def cycle_msg(names: List[String]): String = |
31 private def cycle_msg(names: List[Document.Node.Name]): String = |
32 "Cyclic dependency of " + show_path(names) |
32 "Cyclic dependency of " + show_path(names) |
33 |
33 |
34 private def required_by(s: String, initiators: List[String]): String = |
34 private def required_by(initiators: List[Document.Node.Name]): String = |
35 if (initiators.isEmpty) "" |
35 if (initiators.isEmpty) "" |
36 else s + "(required by " + show_path(initiators.reverse) + ")" |
36 else "\n(required by " + show_path(initiators.reverse) + ")" |
37 |
37 |
38 |
38 |
39 /* dependencies */ |
39 /* dependencies */ |
40 |
40 |
41 type Deps = Map[String, Document.Node_Header] |
41 def import_name(master_dir: String, str: String): Document.Node.Name = |
|
42 { |
|
43 val path = Path.explode(str) |
|
44 val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path)) |
|
45 val master_dir1 = thy_load.append(master_dir, path.dir) |
|
46 Document.Node.Name(node_name, master_dir1, path.base.implode) |
|
47 } |
42 |
48 |
43 private def require_thys(initiators: List[String], |
49 type Deps = Map[Document.Node.Name, Document.Node_Header] |
44 deps: Deps, thys: List[(String, String)]): Deps = |
|
45 (deps /: thys)(require_thy(initiators, _, _)) |
|
46 |
50 |
47 private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps = |
51 private def require_thys(initiators: List[Document.Node.Name], |
|
52 deps: Deps, names: List[Document.Node.Name]): Deps = |
|
53 (deps /: names)(require_thy(initiators, _, _)) |
|
54 |
|
55 private def require_thy(initiators: List[Document.Node.Name], |
|
56 deps: Deps, name: Document.Node.Name): Deps = |
48 { |
57 { |
49 val (dir, str) = thy |
58 if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps |
50 val path = Path.explode(str) |
|
51 val thy_name = path.base.implode |
|
52 val node_name = thy_load.append(dir, Thy_Header.thy_path(path)) |
|
53 |
|
54 if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps |
|
55 else { |
59 else { |
56 val dir1 = thy_load.append(dir, path.dir) |
|
57 try { |
60 try { |
58 if (initiators.contains(node_name)) error(cycle_msg(initiators)) |
61 if (initiators.contains(name)) error(cycle_msg(initiators)) |
59 val header = |
62 val header = |
60 try { thy_load.check_thy(node_name) } |
63 try { thy_load.check_thy(name) } |
61 catch { |
64 catch { |
62 case ERROR(msg) => |
65 case ERROR(msg) => |
63 cat_error(msg, "The error(s) above occurred while examining theory file " + |
66 cat_error(msg, "The error(s) above occurred while examining theory " + |
64 quote(node_name) + required_by("\n", initiators)) |
67 quote(name.theory) + required_by(initiators)) |
65 } |
68 } |
66 val thys = header.imports.map(str => (dir1, str)) |
69 val imports = header.imports.map(import_name(name.master_dir, _)) |
67 require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys) |
70 require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports) |
68 } |
71 } |
69 catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) } |
72 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } |
70 } |
73 } |
71 } |
74 } |
72 |
75 |
73 def dependencies(thys: List[(String, String)]): Deps = |
76 def dependencies(names: List[Document.Node.Name]): Deps = |
74 require_thys(Nil, Map.empty, thys) |
77 require_thys(Nil, Map.empty, names) |
75 } |
78 } |