author | wenzelm |
Fri, 07 Dec 2012 13:56:01 +0100 | |
changeset 50415 | 0d60de55c58a |
parent 50414 | e17a1f179bb0 |
child 50424 | 7c8ce63a3c00 |
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 |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
13 |
class Thy_Info(thy_load: Thy_Load) |
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, |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
32 |
header0: Document.Node.Header, |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
33 |
future_header: JFuture[Exn.Result[Document.Node.Header]]) |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
34 |
{ |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
35 |
def join_header: Document.Node.Header = Exn.release(future_header.get) |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
36 |
} |
48872 | 37 |
|
38 |
object Dependencies |
|
39 |
{ |
|
48873 | 40 |
val empty = new Dependencies(Nil, Nil, Set.empty) |
48872 | 41 |
} |
42 |
||
43 |
final class Dependencies private( |
|
44 |
rev_deps: List[Dep], |
|
48873 | 45 |
val keywords: Thy_Header.Keywords, |
48872 | 46 |
val seen: Set[Document.Node.Name]) |
48871 | 47 |
{ |
48873 | 48 |
def :: (dep: Dep): Dependencies = |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
49 |
new Dependencies(dep :: rev_deps, dep.header0.keywords ::: keywords, seen) |
48873 | 50 |
|
51 |
def + (name: Document.Node.Name): Dependencies = |
|
52 |
new Dependencies(rev_deps, keywords, seen = seen + name) |
|
48872 | 53 |
|
54 |
def deps: List[Dep] = rev_deps.reverse |
|
55 |
||
56 |
def loaded_theories: Set[String] = |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
57 |
(thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory } |
48872 | 58 |
|
48883 | 59 |
def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) |
48871 | 60 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
61 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
62 |
private def require_thys(files: Boolean, initiators: List[Document.Node.Name], |
48872 | 63 |
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
|
64 |
(required /: names)(require_thy(files, initiators, _, _)) |
44615 | 65 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
66 |
private def require_thy(files: Boolean, initiators: List[Document.Node.Name], |
48872 | 67 |
required: Dependencies, name: Document.Node.Name): Dependencies = |
44615 | 68 |
{ |
48871 | 69 |
if (required.seen(name)) required |
70 |
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
|
71 |
else { |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
72 |
def err(msg: String): Nothing = |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
73 |
cat_error(msg, "The error(s) above occurred while examining theory " + |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
74 |
quote(name.theory) + required_by(initiators)) |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
75 |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
76 |
try { |
44615 | 77 |
if (initiators.contains(name)) error(cycle_msg(initiators)) |
48883 | 78 |
val syntax = required.make_syntax |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
79 |
|
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
80 |
val header0 = |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
81 |
try { thy_load.check_thy(name) } |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
82 |
catch { case ERROR(msg) => err(msg) } |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
83 |
|
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
84 |
val future_header: JFuture[Exn.Result[Document.Node.Header]] = |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
85 |
if (files) { |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
86 |
val string = thy_load.with_thy_text(name, _.toString) |
50415 | 87 |
val syntax0 = syntax.add_keywords(header0.keywords) |
88 |
||
89 |
if (thy_load.body_files_test(syntax0, string)) { |
|
90 |
default_thread_pool.submit(() => |
|
91 |
Exn.capture { |
|
92 |
try { |
|
93 |
val files = thy_load.body_files(syntax0, string) |
|
94 |
header0.copy(uses = header0.uses ::: files.map((_, false))) |
|
95 |
} |
|
96 |
catch { case ERROR(msg) => err(msg) } |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
97 |
} |
50415 | 98 |
) |
99 |
} |
|
100 |
else Library.future_value(Exn.Res(header0)) |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
101 |
} |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
102 |
else Library.future_value(Exn.Res(header0)) |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
103 |
|
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
104 |
Dep(name, header0, future_header) :: |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
105 |
require_thys(files, name :: initiators, required + name, header0.imports) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
106 |
} |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
107 |
catch { |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
108 |
case e: Throwable => |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
109 |
val bad_header = Document.Node.bad_header(Exn.message(e)) |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
49098
diff
changeset
|
110 |
Dep(name, bad_header, Library.future_value(Exn.Res(bad_header))) :: (required + name) |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
46737
diff
changeset
|
111 |
} |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
112 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
113 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
114 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48885
diff
changeset
|
115 |
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
|
116 |
require_thys(inlined_files, Nil, Dependencies.empty, names) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
117 |
} |