author | wenzelm |
Tue, 18 Mar 2014 17:39:03 +0100 | |
changeset 56208 | 06cc31dff138 |
parent 55879 | src/Pure/Thy/thy_load.scala@ac979f750c1a |
child 56209 | 3c89e21d9be2 |
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 |
{ |
50204
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
17 |
/* paths */ |
daeb1674fb91
tuned signature -- avoid intrusion of module Path in generic PIDE concepts;
wenzelm
parents:
48889
diff
changeset
|
18 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
19 |
def thy_path(path: Path): Path = path.ext("thy") |
48484 | 20 |
|
56208 | 21 |
def is_wellformed_thy_path(str: String): Boolean = |
48484 | 22 |
try { thy_path(Path.explode(str)); true } |
23 |
catch { case ERROR(_) => false } |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
24 |
} |
44953 | 25 |
|
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48409
diff
changeset
|
26 |
|
56208 | 27 |
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
|
28 |
{ |
54514 | 29 |
/* document node names */ |
30 |
||
31 |
def node_name(raw_path: Path): Document.Node.Name = |
|
32 |
{ |
|
33 |
val path = raw_path.expand |
|
34 |
val node = path.implode |
|
35 |
val theory = Thy_Header.thy_name(node).getOrElse("") |
|
54515 | 36 |
val master_dir = if (theory == "") "" else path.dir.implode |
37 |
Document.Node.Name(node, master_dir, theory) |
|
54514 | 38 |
} |
39 |
||
40 |
||
44953 | 41 |
/* file-system operations */ |
42 |
||
43 |
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
|
44 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 45 |
|
48885 | 46 |
def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
47 |
{ |
|
48 |
val path = Path.explode(name.node) |
|
49 |
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
|
50 |
|
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
|
51 |
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
|
52 |
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
|
53 |
f(text) |
48885 | 54 |
} |
55 |
||
46737 | 56 |
|
57 |
/* theory files */ |
|
58 |
||
50415 | 59 |
def body_files_test(syntax: Outer_Syntax, text: String): Boolean = |
60 |
syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) |
|
61 |
||
62 |
def body_files(syntax: Outer_Syntax, text: String): List[String] = |
|
48885 | 63 |
{ |
50415 | 64 |
val spans = Thy_Syntax.parse_spans(syntax.scan(text)) |
54513 | 65 |
spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList |
48885 | 66 |
} |
67 |
||
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
|
68 |
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
|
69 |
{ |
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
|
70 |
val theory = Thy_Header.base_name(s) |
54515 | 71 |
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
|
72 |
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
|
73 |
val path = Path.explode(s) |
56208 | 74 |
val node = append(master.master_dir, Resources.thy_path(path)) |
54515 | 75 |
val master_dir = append(master.master_dir, path.dir) |
76 |
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
|
77 |
} |
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
|
78 |
} |
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
|
79 |
|
48885 | 80 |
def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header = |
46737 | 81 |
{ |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
82 |
try { |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
83 |
val header = Thy_Header.read(text) |
48885 | 84 |
|
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
85 |
val name1 = header.name |
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
86 |
if (name.theory != name1) |
56208 | 87 |
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
|
88 |
" for theory " + quote(name1)) |
48885 | 89 |
|
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
|
90 |
val imports = header.imports.map(import_name(name, _)) |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50641
diff
changeset
|
91 |
Document.Node.Header(imports, header.keywords, Nil) |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
92 |
} |
50641 | 93 |
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
46737 | 94 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
95 |
|
48885 | 96 |
def check_thy(name: Document.Node.Name): Document.Node.Header = |
97 |
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
|
98 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
99 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
100 |
/* theory text edits */ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
101 |
|
54521
744ea0025e11
clarified Document.Blobs environment vs. actual edits of auxiliary files;
wenzelm
parents:
54519
diff
changeset
|
102 |
def text_edits( |
744ea0025e11
clarified Document.Blobs environment vs. actual edits of auxiliary files;
wenzelm
parents:
54519
diff
changeset
|
103 |
reparse_limit: Int, |
744ea0025e11
clarified Document.Blobs environment vs. actual edits of auxiliary files;
wenzelm
parents:
54519
diff
changeset
|
104 |
previous: Document.Version, |
744ea0025e11
clarified Document.Blobs environment vs. actual edits of auxiliary files;
wenzelm
parents:
54519
diff
changeset
|
105 |
doc_blobs: Document.Blobs, |
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54521
diff
changeset
|
106 |
edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) = |
54521
744ea0025e11
clarified Document.Blobs environment vs. actual edits of auxiliary files;
wenzelm
parents:
54519
diff
changeset
|
107 |
Thy_Syntax.text_edits(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
|
108 |
|
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54521
diff
changeset
|
109 |
def syntax_changed() { } |
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 |