author | hoelzl |
Wed, 02 Apr 2014 18:35:01 +0200 | |
changeset 56369 | 2704ca85be98 |
parent 56208 | 06cc31dff138 |
child 56392 | bc118a32a870 |
permissions | -rw-r--r-- |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/thy_info.scala |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
3 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
4 |
Theory and file dependencies. |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
6 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
8 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
9 |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
10 |
import java.util.concurrent.{Future => JFuture} |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
11 |
|
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
12 |
|
56208 | 13 |
class Thy_Info(resources: Resources) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
14 |
{ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
15 |
/* messages */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
16 |
|
44615 | 17 |
private def show_path(names: List[Document.Node.Name]): String = |
18 |
names.map(name => quote(name.theory)).mkString(" via ") |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
19 |
|
44615 | 20 |
private def cycle_msg(names: List[Document.Node.Name]): String = |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
21 |
"Cyclic dependency of " + show_path(names) |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
22 |
|
44615 | 23 |
private def required_by(initiators: List[Document.Node.Name]): String = |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
24 |
if (initiators.isEmpty) "" |
44615 | 25 |
else "\n(required by " + show_path(initiators.reverse) + ")" |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
26 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
27 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
28 |
/* dependencies */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
29 |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
30 |
sealed case class Dep( |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
31 |
name: Document.Node.Name, |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
32 |
header: Document.Node.Header) |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
33 |
{ |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
34 |
def load_files(syntax: Outer_Syntax): List[String] = |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
35 |
{ |
56208 | 36 |
val string = resources.with_thy_text(name, _.toString) |
37 |
if (resources.body_files_test(syntax, string)) |
|
38 |
resources.body_files(syntax, string) |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
39 |
else Nil |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
40 |
} |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
41 |
} |
48872 | 42 |
|
43 |
object Dependencies |
|
44 |
{ |
|
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
45 |
val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty) |
48872 | 46 |
} |
47 |
||
48 |
final class Dependencies private( |
|
49 |
rev_deps: List[Dep], |
|
48873 | 50 |
val keywords: Thy_Header.Keywords, |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
51 |
val seen_names: Multi_Map[String, Document.Node.Name], |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
52 |
val seen_positions: Multi_Map[String, Position.T]) |
48871 | 53 |
{ |
48873 | 54 |
def :: (dep: Dep): Dependencies = |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
55 |
new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
56 |
seen_names, seen_positions) |
48873 | 57 |
|
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
58 |
def + (thy: (Document.Node.Name, Position.T)): Dependencies = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
59 |
{ |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
60 |
val (name, pos) = thy |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
61 |
new Dependencies(rev_deps, keywords, |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
62 |
seen_names + (name.theory -> name), |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
63 |
seen_positions + (name.theory -> pos)) |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
64 |
} |
48872 | 65 |
|
66 |
def deps: List[Dep] = rev_deps.reverse |
|
67 |
||
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
68 |
def errors: List[String] = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
69 |
{ |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
70 |
val header_errors = deps.flatMap(dep => dep.header.errors) |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
71 |
val import_errors = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
72 |
(for { |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
73 |
(theory, names) <- seen_names.iterator_list |
56208 | 74 |
if !resources.loaded_theories(theory) |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
75 |
if names.length > 1 |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
76 |
} yield |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
77 |
"Incoherent imports for theory " + quote(theory) + ":\n" + |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
78 |
cat_lines(names.flatMap(name => |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
79 |
seen_positions.get_list(theory).map(pos => |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
80 |
" " + quote(name.node) + Position.here(pos)))) |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
81 |
).toList |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
82 |
header_errors ::: import_errors |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
83 |
} |
54549
2a3053472ec3
actually expose errors of cumulative theory dependencies;
wenzelm
parents:
54515
diff
changeset
|
84 |
|
56208 | 85 |
lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords) |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
86 |
|
48872 | 87 |
def loaded_theories: Set[String] = |
56208 | 88 |
(resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } |
48872 | 89 |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
90 |
def load_files: List[Path] = |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
91 |
{ |
51298
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
92 |
val dep_files = |
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
93 |
rev_deps.par.map(dep => |
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
94 |
Exn.capture { |
54515 | 95 |
dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) |
51298
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
96 |
}).toList |
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
97 |
((Nil: List[Path]) /: dep_files) { |
ec7f10155389
parallel dep.load_files saves approx. 1s on 4 cores;
wenzelm
parents:
51294
diff
changeset
|
98 |
case (acc_files, files) => Exn.release(files) ::: acc_files |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
99 |
} |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
100 |
} |
48871 | 101 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
102 |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
103 |
private def require_thys(initiators: List[Document.Node.Name], |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
104 |
required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
105 |
(required /: thys)(require_thy(initiators, _, _)) |
44615 | 106 |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
107 |
private def require_thy(initiators: List[Document.Node.Name], |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
108 |
required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies = |
44615 | 109 |
{ |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
110 |
val (name, require_pos) = thy |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
111 |
val theory = name.theory |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
112 |
|
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
113 |
def message: String = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
114 |
"The error(s) above occurred for theory " + quote(theory) + |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
115 |
required_by(initiators) + Position.here(require_pos) |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
116 |
|
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
117 |
val required1 = required + thy |
56208 | 118 |
if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory)) |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
119 |
required1 |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
120 |
else { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
121 |
try { |
44615 | 122 |
if (initiators.contains(name)) error(cycle_msg(initiators)) |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
123 |
val header = |
56208 | 124 |
try { resources.check_thy(name).cat_errors(message) } |
54549
2a3053472ec3
actually expose errors of cumulative theory dependencies;
wenzelm
parents:
54515
diff
changeset
|
125 |
catch { case ERROR(msg) => cat_error(msg, message) } |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
126 |
val imports = header.imports.map((_, Position.File(name.node))) |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
127 |
Dep(name, header) :: require_thys(name :: initiators, required1, imports) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
128 |
} |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
129 |
catch { |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
130 |
case e: Throwable => |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
131 |
Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
132 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
133 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
134 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
135 |
|
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
136 |
def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
137 |
require_thys(Nil, Dependencies.empty, thys) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
138 |
} |