author | wenzelm |
Sat, 17 Sep 2011 17:55:39 +0200 | |
changeset 44953 | cdfe42f1267c |
parent 44616 | 4beeaf2a226d |
child 46737 | 09ab89658a5d |
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 |
|
10 |
import java.io.File |
|
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 |
||
32 |
def check_thy(name: Document.Node.Name): Thy_Header = |
|
33 |
{ |
|
34 |
val file = new File(name.node) |
|
35 |
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
|
36 |
Thy_Header.read(file) |
|
37 |
} |
|
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 |