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(resources: Resources) |
|
11 { |
|
12 /* messages */ |
|
13 |
|
14 private def show_path(names: List[Document.Node.Name]): String = |
|
15 names.map(name => quote(name.theory)).mkString(" via ") |
|
16 |
|
17 private def cycle_msg(names: List[Document.Node.Name]): String = |
|
18 "Cyclic dependency of " + show_path(names) |
|
19 |
|
20 private def required_by(initiators: List[Document.Node.Name]): String = |
|
21 if (initiators.isEmpty) "" |
|
22 else "\n(required by " + show_path(initiators.reverse) + ")" |
|
23 |
|
24 |
|
25 /* dependencies */ |
|
26 |
|
27 object Dependencies |
|
28 { |
|
29 val empty = new Dependencies(Nil, Set.empty) |
|
30 } |
|
31 |
|
32 final class Dependencies private( |
|
33 rev_entries: List[Document.Node.Entry], |
|
34 val seen: Set[Document.Node.Name]) |
|
35 { |
|
36 def :: (entry: Document.Node.Entry): Dependencies = |
|
37 new Dependencies(entry :: rev_entries, seen) |
|
38 |
|
39 def + (name: Document.Node.Name): Dependencies = |
|
40 new Dependencies(rev_entries, seen + name) |
|
41 |
|
42 def entries: List[Document.Node.Entry] = rev_entries.reverse |
|
43 def names: List[Document.Node.Name] = entries.map(_.name) |
|
44 |
|
45 def errors: List[String] = entries.flatMap(_.header.errors) |
|
46 |
|
47 lazy val loaded_theories: Graph[String, Outer_Syntax] = |
|
48 (resources.session_base.loaded_theories /: entries)({ case (graph, entry) => |
|
49 val name = entry.name.theory |
|
50 val imports = entry.header.imports.map(p => p._1.theory) |
|
51 |
|
52 val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) |
|
53 val graph2 = (graph1 /: imports)(_.add_edge(_, name)) |
|
54 |
|
55 val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil |
|
56 val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_)) |
|
57 val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header |
|
58 |
|
59 graph2.map_node(name, _ => syntax) |
|
60 }) |
|
61 |
|
62 def loaded_files: List[(String, List[Path])] = |
|
63 { |
|
64 names.map(_.theory) zip |
|
65 Par_List.map((e: () => List[Path]) => e(), |
|
66 names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) |
|
67 } |
|
68 |
|
69 def imported_files: List[Path] = |
|
70 { |
|
71 val base = resources.session_base |
|
72 val base_theories = |
|
73 loaded_theories.all_preds(names.map(_.theory)). |
|
74 filter(base.loaded_theories.defined(_)) |
|
75 |
|
76 base_theories.map(theory => base.known.theories(theory).path) ::: |
|
77 base_theories.flatMap(base.known.loaded_files(_)) |
|
78 } |
|
79 |
|
80 lazy val overall_syntax: Outer_Syntax = |
|
81 Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_))) |
|
82 |
|
83 override def toString: String = entries.toString |
|
84 } |
|
85 |
|
86 private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
|
87 thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
|
88 (required /: thys)(require_thy(initiators, _, _)) |
|
89 |
|
90 private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, |
|
91 thy: (Document.Node.Name, Position.T)): Dependencies = |
|
92 { |
|
93 val (name, pos) = thy |
|
94 |
|
95 def message: String = |
|
96 "The error(s) above occurred for theory " + quote(name.theory) + |
|
97 required_by(initiators) + Position.here(pos) |
|
98 |
|
99 val required1 = required + name |
|
100 if (required.seen(name)) required |
|
101 else if (resources.session_base.loaded_theory(name)) required1 |
|
102 else { |
|
103 try { |
|
104 if (initiators.contains(name)) error(cycle_msg(initiators)) |
|
105 val header = |
|
106 try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
|
107 catch { case ERROR(msg) => cat_error(msg, message) } |
|
108 Document.Node.Entry(name, header) :: |
|
109 require_thys(name :: initiators, required1, header.imports) |
|
110 } |
|
111 catch { |
|
112 case e: Throwable => |
|
113 Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
|
114 } |
|
115 } |
|
116 } |
|
117 |
|
118 def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
|
119 require_thys(Nil, Dependencies.empty, thys) |
|
120 } |
|