|
1 /* Title: Pure/Thy/thy_info.scala |
|
2 Author: Makarius |
|
3 |
|
4 Theory and file dependencies. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 class Thy_Info(thy_load: Thy_Load) |
|
11 { |
|
12 /* messages */ |
|
13 |
|
14 private def show_path(names: List[String]): String = |
|
15 names.map(Library.quote).mkString(" via ") |
|
16 |
|
17 private def cycle_msg(names: List[String]): String = |
|
18 "Cyclic dependency of " + show_path(names) |
|
19 |
|
20 private def required_by(s: String, initiators: List[String]): String = |
|
21 if (initiators.isEmpty) "" |
|
22 else s + "(required by " + show_path(initiators.reverse) + ")" |
|
23 |
|
24 |
|
25 /* dependencies */ |
|
26 |
|
27 type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header) |
|
28 |
|
29 private def require_thys( |
|
30 initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps = |
|
31 (deps /: strs)(require_thy(initiators, dir, _, _)) |
|
32 |
|
33 private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps = |
|
34 { |
|
35 val path = Path.explode(str) |
|
36 val name = path.base.implode |
|
37 |
|
38 if (deps.isDefinedAt(name)) deps |
|
39 else { |
|
40 val dir1 = dir + path.dir |
|
41 try { |
|
42 if (initiators.contains(name)) error(cycle_msg(initiators)) |
|
43 val (text, header) = |
|
44 try { thy_load.check_thy(dir1, name) } |
|
45 catch { |
|
46 case ERROR(msg) => |
|
47 cat_error(msg, "The error(s) above occurred while examining theory " + |
|
48 Library.quote(name) + required_by("\n", initiators)) |
|
49 } |
|
50 require_thys(name :: initiators, dir1, |
|
51 deps + (name -> Exn.Res(text, header)), header.imports) |
|
52 } |
|
53 catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } |
|
54 } |
|
55 } |
|
56 |
|
57 def dependencies(dir: Path, str: String): Deps = |
|
58 require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??) |
|
59 } |