author | wenzelm |
Mon, 28 Nov 2011 22:05:32 +0100 | |
changeset 45666 | d83797ef0d2d |
parent 44954 | b536b1144eb3 |
child 46122 | 1e9ec1a44dfc |
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 |
|
43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
10 |
object Thy_Info |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
11 |
{ |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
12 |
/* protocol messages */ |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
13 |
|
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
14 |
object Loaded_Theory { |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
15 |
def unapply(msg: XML.Tree): Option[String] = |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
16 |
msg match { |
45666 | 17 |
case XML.Elem(Markup(Isabelle_Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => |
18 |
Some(name) |
|
43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
19 |
case _ => None |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
20 |
} |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
21 |
} |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
22 |
} |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
23 |
|
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43652
diff
changeset
|
24 |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
25 |
class Thy_Info(thy_load: Thy_Load) |
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 |
/* messages */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
28 |
|
44615 | 29 |
private def show_path(names: List[Document.Node.Name]): String = |
30 |
names.map(name => quote(name.theory)).mkString(" via ") |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
31 |
|
44615 | 32 |
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
|
33 |
"Cyclic dependency of " + show_path(names) |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
34 |
|
44615 | 35 |
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
|
36 |
if (initiators.isEmpty) "" |
44615 | 37 |
else "\n(required by " + show_path(initiators.reverse) + ")" |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
38 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
39 |
|
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
40 |
/* dependencies */ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
41 |
|
44616 | 42 |
def import_name(dir: String, str: String): Document.Node.Name = |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
43 |
{ |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
44 |
val path = Path.explode(str) |
44616 | 45 |
val node = thy_load.append(dir, Thy_Header.thy_path(path)) |
46 |
val dir1 = thy_load.append(dir, path.dir) |
|
47 |
val theory = path.base.implode |
|
48 |
Document.Node.Name(node, dir1, theory) |
|
44615 | 49 |
} |
50 |
||
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
51 |
type Dep = (Document.Node.Name, Document.Node_Header) |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
52 |
private type Required = (List[Dep], Set[Document.Node.Name]) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
53 |
|
44615 | 54 |
private def require_thys(initiators: List[Document.Node.Name], |
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
55 |
required: Required, names: List[Document.Node.Name]): Required = |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
56 |
(required /: names)(require_thy(initiators, _, _)) |
44615 | 57 |
|
58 |
private def require_thy(initiators: List[Document.Node.Name], |
|
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
59 |
required: Required, name: Document.Node.Name): Required = |
44615 | 60 |
{ |
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
61 |
val (deps, seen) = required |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
62 |
if (seen(name)) required |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
63 |
else if (thy_load.is_loaded(name.theory)) (deps, seen + name) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
64 |
else { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
65 |
try { |
44615 | 66 |
if (initiators.contains(name)) error(cycle_msg(initiators)) |
44574 | 67 |
val header = |
44615 | 68 |
try { thy_load.check_thy(name) } |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
69 |
catch { |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
70 |
case ERROR(msg) => |
44615 | 71 |
cat_error(msg, "The error(s) above occurred while examining theory " + |
72 |
quote(name.theory) + required_by(initiators)) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
73 |
} |
44616 | 74 |
val imports = header.imports.map(import_name(name.dir, _)) |
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
75 |
val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports) |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
76 |
((name, Exn.Res(header)) :: deps1, seen1) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
77 |
} |
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
78 |
catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) } |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
79 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
80 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
81 |
|
44954
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
82 |
def dependencies(names: List[Document.Node.Name]): List[Dep] = |
b536b1144eb3
more careful traversal of theory dependencies to retain standard import order;
wenzelm
parents:
44616
diff
changeset
|
83 |
require_thys(Nil, (Nil, Set.empty), names)._1.reverse |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
84 |
} |