author | wenzelm |
Fri, 20 Jul 2012 22:29:25 +0200 | |
changeset 48409 | 0d2114eb412a |
parent 46938 | cda018294515 |
child 48422 | 9613780a805b |
permissions | -rw-r--r-- |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/thy_load.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 |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
4 |
Primitives for loading theory files. |
43651
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 |
|
44953 | 9 |
|
48409 | 10 |
import java.io.{File => JFile} |
44953 | 11 |
|
12 |
||
13 |
||
14 |
class Thy_Load |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
15 |
{ |
44953 | 16 |
/* loaded theories provided by prover */ |
17 |
||
18 |
private var loaded_theories: Set[String] = Set() |
|
19 |
||
20 |
def register_thy(thy_name: String): Unit = |
|
21 |
synchronized { loaded_theories += thy_name } |
|
22 |
||
23 |
def is_loaded(thy_name: String): Boolean = |
|
24 |
synchronized { loaded_theories.contains(thy_name) } |
|
25 |
||
26 |
||
27 |
/* file-system operations */ |
|
28 |
||
29 |
def append(dir: String, source_path: Path): String = |
|
30 |
(Path.explode(dir) + source_path).implode |
|
31 |
||
46737 | 32 |
def read_header(name: Document.Node.Name): Thy_Header = |
44953 | 33 |
{ |
48409 | 34 |
val file = new JFile(name.node) |
44953 | 35 |
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
36 |
Thy_Header.read(file) |
|
37 |
} |
|
46737 | 38 |
|
39 |
||
40 |
/* theory files */ |
|
41 |
||
42 |
def thy_path(path: Path): Path = path.ext("thy") |
|
43 |
||
44 |
private def import_name(dir: String, s: String): Document.Node.Name = |
|
45 |
{ |
|
46 |
val theory = Thy_Header.base_name(s) |
|
47 |
if (is_loaded(theory)) Document.Node.Name(theory, "", theory) |
|
48 |
else { |
|
49 |
val path = Path.explode(s) |
|
50 |
val node = append(dir, thy_path(path)) |
|
51 |
val dir1 = append(dir, path.dir) |
|
52 |
Document.Node.Name(node, dir1, theory) |
|
53 |
} |
|
54 |
} |
|
55 |
||
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
56 |
def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps = |
46737 | 57 |
{ |
58 |
val name1 = header.name |
|
59 |
val imports = header.imports.map(import_name(name.dir, _)) |
|
46770
44c28a33c461
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents:
46748
diff
changeset
|
60 |
// FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2)) |
44c28a33c461
retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
wenzelm
parents:
46748
diff
changeset
|
61 |
val uses = header.uses |
46737 | 62 |
if (name.theory != name1) |
63 |
error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1)) |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46770
diff
changeset
|
64 |
Document.Node.Deps(imports, header.keywords, uses) |
46737 | 65 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
66 |
|
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
67 |
def check_thy(name: Document.Node.Name): Document.Node.Deps = |
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
68 |
check_header(name, read_header(name)) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
69 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
70 |