author | wenzelm |
Thu, 31 May 2018 22:27:13 +0200 | |
changeset 68336 | 09ac56914b29 |
parent 68317 | 938803796a8b |
child 68381 | 2fd3a6d6ba2e |
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 |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
11 |
import scala.util.parsing.input.Reader |
48885 | 12 |
|
48409 | 13 |
import java.io.{File => JFile} |
44953 | 14 |
|
15 |
||
65359 | 16 |
class Resources( |
65361 | 17 |
val session_base: Sessions.Base, |
65359 | 18 |
val log: Logger = No_Logger) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
19 |
{ |
66959 | 20 |
resources => |
64839 | 21 |
|
65250 | 22 |
def thy_path(path: Path): Path = path.ext("thy") |
23 |
||
64839 | 24 |
|
44953 | 25 |
/* file-system operations */ |
26 |
||
27 |
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
|
28 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 29 |
|
65488 | 30 |
def append(node_name: Document.Node.Name, source_path: Path): String = |
31 |
append(node_name.master_dir, source_path) |
|
32 |
||
46737 | 33 |
|
64657 | 34 |
/* source files of Isabelle/ML bootstrap */ |
35 |
||
36 |
def source_file(raw_name: String): Option[String] = |
|
37 |
{ |
|
38 |
if (Path.is_wellformed(raw_name)) { |
|
39 |
if (Path.is_valid(raw_name)) { |
|
40 |
def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None |
|
41 |
||
42 |
val path = Path.explode(raw_name) |
|
43 |
val path1 = |
|
44 |
if (path.is_absolute || path.is_current) check(path) |
|
45 |
else { |
|
46 |
check(Path.explode("~~/src/Pure") + path) orElse |
|
47 |
(if (Isabelle_System.getenv("ML_SOURCES") == "") None |
|
48 |
else check(Path.explode("$ML_SOURCES") + path)) |
|
49 |
} |
|
50 |
Some(File.platform_path(path1 getOrElse path)) |
|
51 |
} |
|
52 |
else None |
|
53 |
} |
|
54 |
else Some(raw_name) |
|
55 |
} |
|
56 |
||
57 |
||
46737 | 58 |
/* theory files */ |
59 |
||
66698
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
60 |
def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = |
66695 | 61 |
{ |
66918
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66917
diff
changeset
|
62 |
val (is_utf8, raw_text) = |
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66917
diff
changeset
|
63 |
with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) |
66698
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
64 |
() => { |
66917
fcf84cd6c94f
clarified check, assuming that load commands are plain ASCII;
wenzelm
parents:
66850
diff
changeset
|
65 |
if (syntax.load_commands_in(raw_text)) { |
66918
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66917
diff
changeset
|
66 |
val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) |
66698
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
67 |
val spans = syntax.parse_spans(text) |
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
68 |
val dir = Path.explode(name.master_dir) |
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
69 |
spans.iterator.map(Command.span_files(syntax, _)._1).flatten. |
66700 | 70 |
map(a => (dir + Path.explode(a)).expand).toList |
66698
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
71 |
} |
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
72 |
else Nil |
66696
8f863dae78a0
clarified pure_files, based on uniform loaded_files;
wenzelm
parents:
66695
diff
changeset
|
73 |
} |
66695 | 74 |
} |
75 |
||
66701 | 76 |
def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] = |
77 |
{ |
|
78 |
val roots = |
|
79 |
for { (name, _) <- Thy_Header.ml_roots } |
|
80 |
yield (dir + Path.explode(name)).expand |
|
81 |
val files = |
|
82 |
for { |
|
83 |
(path, (_, theory)) <- roots zip Thy_Header.ml_roots |
|
84 |
file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() |
|
85 |
} yield file |
|
86 |
roots ::: files |
|
87 |
} |
|
66696
8f863dae78a0
clarified pure_files, based on uniform loaded_files;
wenzelm
parents:
66695
diff
changeset
|
88 |
|
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
89 |
def theory_name(qualifier: String, theory: String): String = |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
90 |
if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
91 |
theory |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
92 |
else Long_Name.qualify(qualifier, theory) |
65471
05e5bffcf1d8
clarified loaded_theories: map to qualified theory name;
wenzelm
parents:
65467
diff
changeset
|
93 |
|
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
94 |
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
95 |
{ |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
96 |
val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
97 |
if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
98 |
else { |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
99 |
session_base.known_theory(theory) match { |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
100 |
case Some(node_name) => node_name |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
101 |
case None => |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
102 |
if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
103 |
Document.Node.Name.loaded_theory(theory) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
104 |
else { |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
105 |
val path = Path.explode(s) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
106 |
val node = append(dir, thy_path(path)) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
107 |
val master_dir = append(dir, path.dir) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
108 |
Document.Node.Name(node, master_dir, theory) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
109 |
} |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
110 |
} |
65472 | 111 |
} |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
112 |
} |
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
|
113 |
|
65529 | 114 |
def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |
66966 | 115 |
import_name(session_base.theory_qualifier(name), name.master_dir, s) |
65489 | 116 |
|
66966 | 117 |
def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String = |
66767 | 118 |
{ |
119 |
val name = import_name(qualifier, dir, s) |
|
120 |
val s1 = |
|
121 |
if (session_base.loaded_theory(name)) name.theory |
|
122 |
else { |
|
66850 | 123 |
(try { Some(name.path) } catch { case ERROR(_) => None }) match { |
124 |
case None => s |
|
125 |
case Some(path) => |
|
126 |
session_base.known.get_file(path.file) match { |
|
66966 | 127 |
case Some(name1) if base.theory_qualifier(name1) != qualifier => |
66850 | 128 |
name1.theory |
129 |
case Some(name1) if Thy_Header.is_base_name(s) => |
|
130 |
name1.theory_base_name |
|
131 |
case _ => s |
|
132 |
} |
|
66767 | 133 |
} |
134 |
} |
|
135 |
val name2 = import_name(qualifier, dir, s1) |
|
136 |
if (name.node == name2.node) s1 else s |
|
137 |
} |
|
138 |
||
64656 | 139 |
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
140 |
{ |
|
66771
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
141 |
val path = name.path |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
142 |
if (path.is_file) { |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
143 |
val reader = Scan.byte_reader(path.file) |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
144 |
try { f(reader) } finally { reader.close } |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
145 |
} |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
146 |
else if (name.node == name.theory) |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
147 |
error("Cannot load theory " + quote(name.theory)) |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
148 |
else error ("Cannot load theory file " + path) |
64656 | 149 |
} |
150 |
||
65359 | 151 |
def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], |
152 |
start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header = |
|
46737 | 153 |
{ |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
154 |
if (node_name.is_theory && reader.source.length > 0) { |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
155 |
try { |
66713 | 156 |
val header = Thy_Header.read(reader, start, strict) |
48885 | 157 |
|
65439 | 158 |
val base_name = node_name.theory_base_name |
59694 | 159 |
val (name, pos) = header.name |
160 |
if (base_name != name) |
|
59718 | 161 |
error("Bad theory name " + quote(name) + |
65250 | 162 |
" for file " + thy_path(Path.basic(base_name)) + Position.here(pos) + |
66766 | 163 |
Completion.report_theories(pos, List(base_name))) |
48885 | 164 |
|
67296
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
165 |
val imports = |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
166 |
header.imports.map({ case (s, pos) => |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
167 |
val name = import_name(node_name, s) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
168 |
if (Sessions.exclude_theory(name.theory_base_name)) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
169 |
error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos)) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
170 |
(name, pos) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
171 |
}) |
63579 | 172 |
Document.Node.Header(imports, header.keywords, header.abbrevs) |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
173 |
} |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
174 |
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } |
50414
e17a1f179bb0
explore theory_body_files via future, for improved performance;
wenzelm
parents:
50291
diff
changeset
|
175 |
} |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
176 |
else Document.Node.no_header |
46737 | 177 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
178 |
|
65359 | 179 |
def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command, |
180 |
strict: Boolean = true): Document.Node.Header = |
|
181 |
with_thy_reader(name, check_thy_reader(name, _, start, strict)) |
|
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
182 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
183 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
184 |
/* special header */ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
185 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
186 |
def special_header(name: Document.Node.Name): Option[Document.Node.Header] = |
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
187 |
{ |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
188 |
val imports = |
67215 | 189 |
if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name)) |
190 |
else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) |
|
65489 | 191 |
else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE)) |
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
192 |
else Nil |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
193 |
if (imports.isEmpty) None |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
194 |
else Some(Document.Node.Header(imports.map((_, Position.none)))) |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
195 |
} |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
196 |
|
67287 | 197 |
def is_hidden(name: Document.Node.Name): Boolean = |
67293 | 198 |
!name.is_theory || name.theory == Sessions.root_name || name.is_bibtex_theory |
67287 | 199 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
200 |
|
64797 | 201 |
/* blobs */ |
202 |
||
203 |
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = |
|
204 |
(for { |
|
205 |
(node_name, node) <- nodes.iterator |
|
65361 | 206 |
if !session_base.loaded_theory(node_name) |
64797 | 207 |
cmd <- node.load_commands.iterator |
208 |
name <- cmd.blobs_undefined.iterator |
|
209 |
} yield name).toList |
|
210 |
||
211 |
||
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
212 |
/* document changes */ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
213 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
214 |
def parse_change( |
56315 | 215 |
reparse_limit: Int, |
216 |
previous: Document.Version, |
|
217 |
doc_blobs: Document.Blobs, |
|
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
68317
diff
changeset
|
218 |
edits: List[Document.Edit_Text], |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
68317
diff
changeset
|
219 |
consolidate: Boolean): Session.Change = |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
68317
diff
changeset
|
220 |
Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) |
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54521
diff
changeset
|
221 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
222 |
def commit(change: Session.Change) { } |
66959 | 223 |
|
224 |
||
225 |
/* theory and file dependencies */ |
|
226 |
||
227 |
object Dependencies |
|
228 |
{ |
|
229 |
val empty = new Dependencies(Nil, Set.empty) |
|
230 |
} |
|
231 |
||
232 |
final class Dependencies private( |
|
233 |
rev_entries: List[Document.Node.Entry], |
|
234 |
val seen: Set[Document.Node.Name]) |
|
235 |
{ |
|
236 |
def :: (entry: Document.Node.Entry): Dependencies = |
|
237 |
new Dependencies(entry :: rev_entries, seen) |
|
238 |
||
239 |
def + (name: Document.Node.Name): Dependencies = |
|
240 |
new Dependencies(rev_entries, seen + name) |
|
241 |
||
242 |
def entries: List[Document.Node.Entry] = rev_entries.reverse |
|
67059 | 243 |
def theories: List[Document.Node.Name] = entries.map(_.name) |
66959 | 244 |
|
245 |
def errors: List[String] = entries.flatMap(_.header.errors) |
|
246 |
||
67056 | 247 |
def check_errors: Dependencies = |
248 |
errors match { |
|
249 |
case Nil => this |
|
250 |
case errs => error(cat_lines(errs)) |
|
251 |
} |
|
252 |
||
66959 | 253 |
lazy val loaded_theories: Graph[String, Outer_Syntax] = |
254 |
(session_base.loaded_theories /: entries)({ case (graph, entry) => |
|
255 |
val name = entry.name.theory |
|
256 |
val imports = entry.header.imports.map(p => p._1.theory) |
|
257 |
||
258 |
val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) |
|
259 |
val graph2 = (graph1 /: imports)(_.add_edge(_, name)) |
|
260 |
||
261 |
val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil |
|
262 |
val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_)) |
|
263 |
val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header |
|
264 |
||
265 |
graph2.map_node(name, _ => syntax) |
|
266 |
}) |
|
267 |
||
268 |
def loaded_files: List[(String, List[Path])] = |
|
269 |
{ |
|
67059 | 270 |
theories.map(_.theory) zip |
66959 | 271 |
Par_List.map((e: () => List[Path]) => e(), |
67059 | 272 |
theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) |
66959 | 273 |
} |
274 |
||
275 |
def imported_files: List[Path] = |
|
276 |
{ |
|
277 |
val base_theories = |
|
67059 | 278 |
loaded_theories.all_preds(theories.map(_.theory)). |
66959 | 279 |
filter(session_base.loaded_theories.defined(_)) |
280 |
||
68306
d575281e18d0
clarified signature: Known.theories retains Document.Node.Entry (with header);
wenzelm
parents:
67881
diff
changeset
|
281 |
base_theories.map(theory => session_base.known.theories(theory).name.path) ::: |
66959 | 282 |
base_theories.flatMap(session_base.known.loaded_files(_)) |
283 |
} |
|
284 |
||
285 |
lazy val overall_syntax: Outer_Syntax = |
|
286 |
Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_))) |
|
287 |
||
288 |
override def toString: String = entries.toString |
|
289 |
} |
|
290 |
||
291 |
private def show_path(names: List[Document.Node.Name]): String = |
|
292 |
names.map(name => quote(name.theory)).mkString(" via ") |
|
293 |
||
294 |
private def cycle_msg(names: List[Document.Node.Name]): String = |
|
295 |
"Cyclic dependency of " + show_path(names) |
|
296 |
||
297 |
private def required_by(initiators: List[Document.Node.Name]): String = |
|
298 |
if (initiators.isEmpty) "" |
|
299 |
else "\n(required by " + show_path(initiators.reverse) + ")" |
|
300 |
||
67881 | 301 |
private def require_thy( |
302 |
progress: Progress, |
|
303 |
initiators: List[Document.Node.Name], |
|
68317 | 304 |
dependencies: Dependencies, |
66959 | 305 |
thy: (Document.Node.Name, Position.T)): Dependencies = |
306 |
{ |
|
307 |
val (name, pos) = thy |
|
308 |
||
309 |
def message: String = |
|
310 |
"The error(s) above occurred for theory " + quote(name.theory) + |
|
311 |
required_by(initiators) + Position.here(pos) |
|
312 |
||
68317 | 313 |
if (dependencies.seen(name)) dependencies |
66959 | 314 |
else { |
68317 | 315 |
val dependencies1 = dependencies + name |
316 |
if (session_base.loaded_theory(name)) dependencies1 |
|
67053 | 317 |
else { |
318 |
try { |
|
319 |
if (initiators.contains(name)) error(cycle_msg(initiators)) |
|
67881 | 320 |
|
321 |
progress.expose_interrupt() |
|
67053 | 322 |
val header = |
323 |
try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } |
|
324 |
catch { case ERROR(msg) => cat_error(msg, message) } |
|
325 |
Document.Node.Entry(name, header) :: |
|
68317 | 326 |
require_thys(progress, name :: initiators, dependencies1, header.imports) |
67053 | 327 |
} |
328 |
catch { |
|
329 |
case e: Throwable => |
|
68317 | 330 |
Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: dependencies1 |
67053 | 331 |
} |
66959 | 332 |
} |
333 |
} |
|
334 |
} |
|
335 |
||
67881 | 336 |
private def require_thys( |
337 |
progress: Progress, |
|
338 |
initiators: List[Document.Node.Name], |
|
68317 | 339 |
dependencies: Dependencies, |
66959 | 340 |
thys: List[(Document.Node.Name, Position.T)]): Dependencies = |
68317 | 341 |
(dependencies /: thys)(require_thy(progress, initiators, _, _)) |
66959 | 342 |
|
67881 | 343 |
def dependencies( |
344 |
thys: List[(Document.Node.Name, Position.T)], |
|
345 |
progress: Progress = No_Progress): Dependencies = |
|
346 |
require_thys(progress, Nil, Dependencies.empty, thys) |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
347 |
} |