author | wenzelm |
Fri, 29 Sep 2017 17:28:44 +0200 | |
changeset 66714 | 9fc4e144693c |
parent 66712 | 4c98c929a12a |
child 66715 | 6bced18e2b91 |
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 |
|
56208 | 10 |
class Thy_Info(resources: Resources) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
11 |
{ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
12 |
/* messages */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
13 |
|
44615 | 14 |
private def show_path(names: List[Document.Node.Name]): String = |
15 |
names.map(name => quote(name.theory)).mkString(" via ") |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
16 |
|
44615 | 17 |
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
|
18 |
"Cyclic dependency of " + show_path(names) |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
19 |
|
44615 | 20 |
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
|
21 |
if (initiators.isEmpty) "" |
44615 | 22 |
else "\n(required by " + show_path(initiators.reverse) + ")" |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
23 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
24 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
25 |
/* dependencies */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
26 |
|
48872 | 27 |
object Dependencies |
28 |
{ |
|
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
29 |
val empty = new Dependencies(Nil, Nil, Nil, Set.empty) |
48872 | 30 |
} |
31 |
||
32 |
final class Dependencies private( |
|
66714 | 33 |
rev_entries: List[Document.Node.Entry], |
48873 | 34 |
val keywords: Thy_Header.Keywords, |
63579 | 35 |
val abbrevs: Thy_Header.Abbrevs, |
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
36 |
val seen: Set[Document.Node.Name]) |
48871 | 37 |
{ |
66714 | 38 |
def :: (entry: Document.Node.Entry): Dependencies = |
63579 | 39 |
new Dependencies( |
66714 | 40 |
entry :: rev_entries, |
41 |
entry.header.keywords ::: keywords, |
|
42 |
entry.header.abbrevs ::: abbrevs, |
|
43 |
seen) |
|
48873 | 44 |
|
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
45 |
def + (name: Document.Node.Name): Dependencies = |
66714 | 46 |
new Dependencies(rev_entries, keywords, abbrevs, seen + name) |
48872 | 47 |
|
66714 | 48 |
def entries: List[Document.Node.Entry] = rev_entries.reverse |
48872 | 49 |
|
66714 | 50 |
def errors: List[String] = entries.flatMap(_.header.errors) |
54549
2a3053472ec3
actually expose errors of cumulative theory dependencies;
wenzelm
parents:
54515
diff
changeset
|
51 |
|
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
63579
diff
changeset
|
52 |
lazy val syntax: Outer_Syntax = |
65361 | 53 |
resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs) |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
54 |
|
66712 | 55 |
def loaded_theories: Set[String] = |
66714 | 56 |
resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory) |
48872 | 57 |
|
66701 | 58 |
def loaded_files: List[(String, List[Path])] = |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
59 |
{ |
66714 | 60 |
val names = entries.map(_.name) |
66701 | 61 |
names.map(_.theory) zip |
62 |
Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _))) |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
63 |
} |
62865 | 64 |
|
66714 | 65 |
override def toString: String = entries.toString |
48871 | 66 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
67 |
|
65359 | 68 |
private def require_thys(initiators: List[Document.Node.Name], required: Dependencies, |
69 |
thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
|
70 |
(required /: thys)(require_thy(initiators, _, _)) |
|
44615 | 71 |
|
65359 | 72 |
private def require_thy(initiators: List[Document.Node.Name], required: Dependencies, |
73 |
thy: (Document.Node.Name, Position.T)): Dependencies = |
|
44615 | 74 |
{ |
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
75 |
val (name, pos) = thy |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
76 |
|
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
77 |
def message: String = |
61536
346aa2c5447f
more accurate imports: allow re-uses of base names in PIDE interaction (amending 60c159d490a2);
wenzelm
parents:
60077
diff
changeset
|
78 |
"The error(s) above occurred for theory " + quote(name.theory) + |
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
79 |
required_by(initiators) + Position.here(pos) |
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
54722
diff
changeset
|
80 |
|
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
wenzelm
parents:
66701
diff
changeset
|
81 |
val required1 = required + name |
65403
4a042bf9488e
clarified checks -- avoid duplicated messages (amending 60c159d490a2);
wenzelm
parents:
65361
diff
changeset
|
82 |
if (required.seen(name)) required |
4a042bf9488e
clarified checks -- avoid duplicated messages (amending 60c159d490a2);
wenzelm
parents:
65361
diff
changeset
|
83 |
else if (resources.session_base.loaded_theory(name)) required1 |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
84 |
else { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
85 |
try { |
44615 | 86 |
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
|
87 |
val header = |
65359 | 88 |
try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
54549
2a3053472ec3
actually expose errors of cumulative theory dependencies;
wenzelm
parents:
54515
diff
changeset
|
89 |
catch { case ERROR(msg) => cat_error(msg, message) } |
66714 | 90 |
Document.Node.Entry(name, header) :: |
91 |
require_thys(name :: initiators, required1, header.imports) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
92 |
} |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
93 |
catch { |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
94 |
case e: Throwable => |
66714 | 95 |
Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
96 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
97 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
98 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
99 |
|
65359 | 100 |
def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
101 |
require_thys(Nil, Dependencies.empty, thys) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
102 |
} |