author | wenzelm |
Mon, 26 Nov 2012 10:37:05 +0100 | |
changeset 50210 | 747db833fbf7 |
parent 49098 | 673e0ed547af |
child 50414 | e17a1f179bb0 |
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 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
10 |
class Thy_Info(thy_load: Thy_Load) |
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 |
|
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
27 |
type Dep = (Document.Node.Name, Document.Node.Header) |
48872 | 28 |
|
29 |
object Dependencies |
|
30 |
{ |
|
48873 | 31 |
val empty = new Dependencies(Nil, Nil, Set.empty) |
48872 | 32 |
} |
33 |
||
34 |
final class Dependencies private( |
|
35 |
rev_deps: List[Dep], |
|
48873 | 36 |
val keywords: Thy_Header.Keywords, |
48872 | 37 |
val seen: Set[Document.Node.Name]) |
48871 | 38 |
{ |
48873 | 39 |
def :: (dep: Dep): Dependencies = |
40 |
new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen) |
|
41 |
||
42 |
def + (name: Document.Node.Name): Dependencies = |
|
43 |
new Dependencies(rev_deps, keywords, seen = seen + name) |
|
48872 | 44 |
|
45 |
def deps: List[Dep] = rev_deps.reverse |
|
46 |
||
47 |
def loaded_theories: Set[String] = |
|
48 |
(thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory } |
|
49 |
||
48883 | 50 |
def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) |
48871 | 51 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
52 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
53 |
private def require_thys(files: Boolean, initiators: List[Document.Node.Name], |
48872 | 54 |
required: Dependencies, names: List[Document.Node.Name]): Dependencies = |
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
55 |
(required /: names)(require_thy(files, initiators, _, _)) |
44615 | 56 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
57 |
private def require_thy(files: Boolean, initiators: List[Document.Node.Name], |
48872 | 58 |
required: Dependencies, name: Document.Node.Name): Dependencies = |
44615 | 59 |
{ |
48871 | 60 |
if (required.seen(name)) required |
61 |
else if (thy_load.loaded_theories(name.theory)) required + name |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
62 |
else { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
63 |
try { |
44615 | 64 |
if (initiators.contains(name)) error(cycle_msg(initiators)) |
48883 | 65 |
val syntax = required.make_syntax |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
66 |
val header = |
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
67 |
try { |
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
68 |
if (files) thy_load.check_thy_files(syntax, name) |
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
69 |
else thy_load.check_thy(name) |
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
70 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
71 |
catch { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
72 |
case ERROR(msg) => |
44615 | 73 |
cat_error(msg, "The error(s) above occurred while examining theory " + |
74 |
quote(name.theory) + required_by(initiators)) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
75 |
} |
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
76 |
(name, header) :: require_thys(files, name :: initiators, required + name, header.imports) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
77 |
} |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
78 |
catch { |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
79 |
case e: Throwable => |
48871 | 80 |
(name, Document.Node.bad_header(Exn.message(e))) :: (required + name) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
81 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
82 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
83 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
84 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
85 |
def dependencies(inlined_files: Boolean, names: List[Document.Node.Name]): Dependencies = |
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
86 |
require_thys(inlined_files, Nil, Dependencies.empty, names) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
87 |
} |