author | wenzelm |
Thu, 03 Apr 2014 14:54:17 +0200 | |
changeset 56387 | d92eb5c3960d |
parent 56316 | b1cf8ddc2e04 |
child 56392 | bc118a32a870 |
permissions | -rw-r--r-- |
56208 | 1 |
/* Title: Pure/PIDE/resources.scala |
43651
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 |
|
56208 | 4 |
Resources for theories and auxiliary 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 |
|
48885 | 10 |
import scala.annotation.tailrec |
11 |
||
48409 | 12 |
import java.io.{File => JFile} |
44953 | 13 |
|
14 |
||
56208 | 15 |
object Resources |
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
16 |
{ |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
17 |
def thy_path(path: Path): Path = path.ext("thy") |
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
18 |
} |
44953 | 19 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
20 |
|
56208 | 21 |
class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
22 |
{ |
54514 | 23 |
/* document node names */ |
24 |
||
25 |
def node_name(raw_path: Path): Document.Node.Name = |
|
26 |
{ |
|
27 |
val path = raw_path.expand |
|
28 |
val node = path.implode |
|
29 |
val theory = Thy_Header.thy_name(node).getOrElse("") |
|
54515 | 30 |
val master_dir = if (theory == "") "" else path.dir.implode |
31 |
Document.Node.Name(node, master_dir, theory) |
|
54514 | 32 |
} |
33 |
||
34 |
||
44953 | 35 |
/* file-system operations */ |
36 |
||
37 |
def append(dir: String, source_path: Path): String = |
|
48711
8d381fdef898
need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
wenzelm
parents:
48710
diff
changeset
|
38 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 39 |
|
48885 | 40 |
def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
41 |
{ |
|
42 |
val path = Path.explode(name.node) |
|
43 |
if (!path.is_file) error("No such file: " + path.toString) |
|
50291
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50204
diff
changeset
|
44 |
|
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50204
diff
changeset
|
45 |
val text = File.read(path) |
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50204
diff
changeset
|
46 |
Symbol.decode_strict(text) |
674893679352
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;
wenzelm
parents:
50204
diff
changeset
|
47 |
f(text) |
48885 | 48 |
} |
49 |
||
46737 | 50 |
|
51 |
/* theory files */ |
|
52 |
||
50415 | 53 |
def body_files_test(syntax: Outer_Syntax, text: String): Boolean = |
56314 | 54 |
syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
50415 | 55 |
|
56 |
def body_files(syntax: Outer_Syntax, text: String): List[String] = |
|
48885 | 57 |
{ |
50415 | 58 |
val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
54513 | 59 |
spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |
48885 | 60 |
} |
61 |
||
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
62 |
def import_name(master: Document.Node.Name, s: String): Document.Node.Name = |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
63 |
{ |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
64 |
val theory = Thy_Header.base_name(s) |
54515 | 65 |
if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory) |
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
66 |
else { |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
67 |
val path = Path.explode(s) |
56208 | 68 |
val node = append(master.master_dir, Resources.thy_path(path)) |
54515 | 69 |
val master_dir = append(master.master_dir, path.dir) |
70 |
Document.Node.Name(node, master_dir, theory) |
|
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
71 |
} |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
72 |
} |
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
73 |
|
48885 | 74 |
def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
46737 | 75 |
{ |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
76 |
try { |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
77 |
val header = Thy_Header.read(text) |
48885 | 78 |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
79 |
val name1 = header.name |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
80 |
if (name.theory != name1) |
56208 | 81 |
error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) + |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
82 |
" for theory " + quote(name1)) |
48885 | 83 |
|
51634
553953ad8165
more general Thy_Load.import_name, e.g. relevant for Isabelle/eclipse -- NB: Thy_Load serves as main hub for funny overriding to adapt to provers and editors;
wenzelm
parents:
51293
diff
changeset
|
84 |
val imports = header.imports.map(import_name(name, _)) |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50641
diff
changeset
|
85 |
Document.Node.Header(imports, header.keywords, Nil) |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
86 |
} |
50641 | 87 |
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
46737 | 88 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
89 |
|
48885 | 90 |
def check_thy(name: Document.Node.Name): Document.Node.Header = |
91 |
with_thy_text(name, check_thy_text(name, _)) |
|
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
92 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
93 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
94 |
/* document changes */ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
95 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
96 |
def parse_change( |
56315 | 97 |
reparse_limit: Int, |
98 |
previous: Document.Version, |
|
99 |
doc_blobs: Document.Blobs, |
|
100 |
edits: List[Document.Edit_Text]): Session.Change = |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
101 |
Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) |
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54521
diff
changeset
|
102 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
103 |
def commit(change: Session.Change) { } |
56387 | 104 |
|
105 |
||
106 |
/* prover process */ |
|
107 |
||
108 |
def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover = |
|
109 |
new Isabelle_Process(receiver, args) with Protocol |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
110 |
} |
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
111 |