author | wenzelm |
Wed, 03 Nov 2021 14:26:13 +0100 | |
changeset 74671 | df12779c3ce8 |
parent 73565 | 1aa92bc4d356 |
child 74696 | 0554a5c4c191 |
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 |
|
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
10 |
import scala.util.parsing.input.Reader |
48885 | 11 |
|
48409 | 12 |
import java.io.{File => JFile} |
44953 | 13 |
|
14 |
||
72962 | 15 |
object Resources |
16 |
{ |
|
17 |
def empty: Resources = |
|
18 |
new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) |
|
19 |
} |
|
20 |
||
65359 | 21 |
class Resources( |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
22 |
val sessions_structure: Sessions.Structure, |
65361 | 23 |
val session_base: Sessions.Base, |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
24 |
val log: Logger = No_Logger, |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
25 |
command_timings: List[Properties.T] = Nil) |
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
26 |
{ |
66959 | 27 |
resources => |
64839 | 28 |
|
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
29 |
|
72637 | 30 |
/* init session */ |
31 |
||
32 |
def init_session_yxml: String = |
|
33 |
{ |
|
34 |
import XML.Encode._ |
|
35 |
||
36 |
YXML.string_of_body( |
|
37 |
pair(list(pair(string, properties)), |
|
38 |
pair(list(pair(string, string)), |
|
39 |
pair(list(pair(string, string)), |
|
40 |
pair(list(pair(string, list(string))), |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
41 |
pair(list(properties), |
74671 | 42 |
pair(list(pair(string, properties)), |
73565 | 43 |
pair(list(pair(string, pair(bool, properties))), |
74671 | 44 |
pair(list(pair(string, string)), list(string)))))))))( |
72646 | 45 |
(sessions_structure.session_positions, |
46 |
(sessions_structure.dest_session_directories, |
|
47 |
(sessions_structure.session_chapters, |
|
48 |
(sessions_structure.bibtex_entries, |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
49 |
(command_timings, |
74671 | 50 |
(Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)), |
73565 | 51 |
(Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))), |
72646 | 52 |
(session_base.global_theories.toList, |
74671 | 53 |
session_base.loaded_theories.keys)))))))))) |
72637 | 54 |
} |
55 |
||
56 |
||
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
57 |
/* file formats */ |
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
58 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
59 |
def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = |
71733 | 60 |
File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
61 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
62 |
def make_theory_content(thy_name: Document.Node.Name): Option[String] = |
71733 | 63 |
File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
64 |
|
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
65 |
def is_hidden(name: Document.Node.Name): Boolean = |
71733 | 66 |
!name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69008
diff
changeset
|
67 |
|
72957 | 68 |
def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = |
69 |
File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) |
|
72956 | 70 |
|
64839 | 71 |
|
44953 | 72 |
/* file-system operations */ |
73 |
||
74 |
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
|
75 |
(Path.explode(dir) + source_path).expand.implode |
44953 | 76 |
|
65488 | 77 |
def append(node_name: Document.Node.Name, source_path: Path): String = |
78 |
append(node_name.master_dir, source_path) |
|
79 |
||
72857 | 80 |
def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
81 |
{ |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
82 |
val node = append(dir, file) |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
83 |
val master_dir = append(dir, file.dir) |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
84 |
Document.Node.Name(node, master_dir, theory) |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
85 |
} |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
86 |
|
70716 | 87 |
def loaded_theory_node(theory: String): Document.Node.Name = |
88 |
Document.Node.Name(theory, "", theory) |
|
89 |
||
46737 | 90 |
|
64657 | 91 |
/* source files of Isabelle/ML bootstrap */ |
92 |
||
93 |
def source_file(raw_name: String): Option[String] = |
|
94 |
{ |
|
95 |
if (Path.is_wellformed(raw_name)) { |
|
96 |
if (Path.is_valid(raw_name)) { |
|
97 |
def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None |
|
98 |
||
99 |
val path = Path.explode(raw_name) |
|
100 |
val path1 = |
|
101 |
if (path.is_absolute || path.is_current) check(path) |
|
102 |
else { |
|
103 |
check(Path.explode("~~/src/Pure") + path) orElse |
|
104 |
(if (Isabelle_System.getenv("ML_SOURCES") == "") None |
|
105 |
else check(Path.explode("$ML_SOURCES") + path)) |
|
106 |
} |
|
107 |
Some(File.platform_path(path1 getOrElse path)) |
|
108 |
} |
|
109 |
else None |
|
110 |
} |
|
111 |
else Some(raw_name) |
|
112 |
} |
|
113 |
||
114 |
||
46737 | 115 |
/* theory files */ |
116 |
||
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
117 |
def load_commands(syntax: Outer_Syntax, name: Document.Node.Name) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
118 |
: () => List[Command_Span.Span] = |
66695 | 119 |
{ |
66918
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66917
diff
changeset
|
120 |
val (is_utf8, raw_text) = |
ec2b50aeb0dd
more robust treatment of UTF8 in raw byte sources;
wenzelm
parents:
66917
diff
changeset
|
121 |
with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
122 |
() => |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
123 |
{ |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
124 |
if (syntax.has_load_commands(raw_text)) { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
125 |
val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
126 |
syntax.parse_spans(text).filter(_.is_load_command(syntax)) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
127 |
} |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
128 |
else Nil |
66698
5b9dc3f7bcde
prefer sequential file-system access, but parallel parse;
wenzelm
parents:
66697
diff
changeset
|
129 |
} |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
130 |
} |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
131 |
|
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
132 |
def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span]) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
133 |
: List[Path] = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
134 |
{ |
72817
1c378ab75d48
clarified signature, notably access to blob files;
wenzelm
parents:
72816
diff
changeset
|
135 |
val dir = name.master_dir_path |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
136 |
for { span <- spans; file <- span.loaded_files(syntax).files } |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
137 |
yield (dir + Path.explode(file)).expand |
66695 | 138 |
} |
139 |
||
69560 | 140 |
def pure_files(syntax: Outer_Syntax): List[Path] = |
66701 | 141 |
{ |
69560 | 142 |
val pure_dir = Path.explode("~~/src/Pure") |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
143 |
for { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
144 |
(name, theory) <- Thy_Header.ml_roots |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
145 |
path = (pure_dir + Path.explode(name)).expand |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
146 |
node_name = Document.Node.Name(path.implode, path.dir.implode, theory) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
147 |
file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
148 |
} yield file |
66701 | 149 |
} |
66696
8f863dae78a0
clarified pure_files, based on uniform loaded_files;
wenzelm
parents:
66695
diff
changeset
|
150 |
|
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
else Long_Name.qualify(qualifier, theory) |
65471
05e5bffcf1d8
clarified loaded_theories: map to qualified theory name;
wenzelm
parents:
65467
diff
changeset
|
155 |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
156 |
def find_theory_node(theory: String): Option[Document.Node.Name] = |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
157 |
{ |
72776 | 158 |
val thy_file = Path.basic(Long_Name.base_name(theory)).thy |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
159 |
val session = session_base.theory_qualifier(theory) |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
160 |
val dirs = |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
161 |
sessions_structure.get(session) match { |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
162 |
case Some(info) => info.dirs |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
163 |
case None => Nil |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
164 |
} |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
165 |
dirs.collectFirst({ |
72857 | 166 |
case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) }) |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
167 |
} |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
168 |
|
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
169 |
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
|
170 |
{ |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
67060
diff
changeset
|
171 |
val theory = theory_name(qualifier, Thy_Header.import_name(s)) |
72857 | 172 |
def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory) |
70717
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70716
diff
changeset
|
173 |
|
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70716
diff
changeset
|
174 |
if (!Thy_Header.is_base_name(s)) theory_node |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70716
diff
changeset
|
175 |
else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) |
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
|
176 |
else { |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70682
diff
changeset
|
177 |
find_theory_node(theory) match { |
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
|
178 |
case Some(node_name) => node_name |
70717
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70716
diff
changeset
|
179 |
case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node |
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
|
180 |
} |
65472 | 181 |
} |
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
|
182 |
} |
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
|
183 |
|
65529 | 184 |
def import_name(name: Document.Node.Name, s: String): Document.Node.Name = |
66966 | 185 |
import_name(session_base.theory_qualifier(name), name.master_dir, s) |
65489 | 186 |
|
70633 | 187 |
def import_name(info: Sessions.Info, s: String): Document.Node.Name = |
188 |
import_name(info.name, info.dir.implode, s) |
|
189 |
||
70718
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
190 |
def find_theory(file: JFile): Option[Document.Node.Name] = |
70673
b0172698d0d3
theory_name based on session_directories: no need for expensive all_known;
wenzelm
parents:
70652
diff
changeset
|
191 |
{ |
70718
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
192 |
for { |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
193 |
qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
194 |
theory_base <- proper_string(Thy_Header.theory_name(file.getName)) |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
195 |
theory = theory_name(qualifier, theory_base) |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
196 |
theory_node <- find_theory_node(theory) |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
197 |
if File.eq(theory_node.path.file, file) |
5bb025e24224
clarified inversion of file name to theory name, notably for Windows;
wenzelm
parents:
70717
diff
changeset
|
198 |
} yield theory_node |
70673
b0172698d0d3
theory_name based on session_directories: no need for expensive all_known;
wenzelm
parents:
70652
diff
changeset
|
199 |
} |
b0172698d0d3
theory_name based on session_directories: no need for expensive all_known;
wenzelm
parents:
70652
diff
changeset
|
200 |
|
70713
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
201 |
def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = |
66767 | 202 |
{ |
70713
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
203 |
val context_session = session_base.theory_qualifier(context_name) |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
204 |
val context_dir = |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
205 |
try { Some(context_name.master_dir_path) } |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
206 |
catch { case ERROR(_) => None } |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
207 |
(for { |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
208 |
(session, (info, _)) <- sessions_structure.imports_graph.iterator |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
209 |
dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
210 |
theory <- Thy_Header.try_read_dir(dir).iterator |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
211 |
if Completion.completed(s)(theory) |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
212 |
} yield { |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
213 |
if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
214 |
else Long_Name.qualify(session, theory) |
fd188463066e
clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
wenzelm
parents:
70712
diff
changeset
|
215 |
}).toList.sorted |
66767 | 216 |
} |
217 |
||
64656 | 218 |
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = |
219 |
{ |
|
66771
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
220 |
val path = name.path |
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69255
diff
changeset
|
221 |
if (path.is_file) using(Scan.byte_reader(path.file))(f) |
66771
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
222 |
else if (name.node == name.theory) |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
223 |
error("Cannot load theory " + quote(name.theory)) |
925d10a7a610
clarified error for bad session-qualified imports;
wenzelm
parents:
66767
diff
changeset
|
224 |
else error ("Cannot load theory file " + path) |
64656 | 225 |
} |
226 |
||
72772 | 227 |
def check_thy(node_name: Document.Node.Name, reader: Reader[Char], |
72777
164cb0806d0a
proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents:
72776
diff
changeset
|
228 |
command: Boolean = true, strict: Boolean = true): Document.Node.Header = |
46737 | 229 |
{ |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64825
diff
changeset
|
230 |
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
|
231 |
try { |
72777
164cb0806d0a
proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents:
72776
diff
changeset
|
232 |
val header = Thy_Header.read(node_name, reader, command = command, strict = strict) |
72778 | 233 |
val imports = |
234 |
header.imports.map({ case (s, pos) => |
|
67296
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
235 |
val name = import_name(node_name, s) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
236 |
if (Sessions.exclude_theory(name.theory_base_name)) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
237 |
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
|
238 |
(name, pos) |
888aa91f0556
clarified check, notably for bibtex theory (amending 5f082b1fa9fa);
wenzelm
parents:
67294
diff
changeset
|
239 |
}) |
72778 | 240 |
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
|
241 |
} |
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
242 |
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
|
243 |
} |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
56913
diff
changeset
|
244 |
else Document.Node.no_header |
46737 | 245 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46737
diff
changeset
|
246 |
|
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
247 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
248 |
/* special header */ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
249 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
250 |
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
|
251 |
{ |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
252 |
val imports = |
67215 | 253 |
if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name)) |
254 |
else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) |
|
65489 | 255 |
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
|
256 |
else Nil |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
257 |
if (imports.isEmpty) None |
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65441
diff
changeset
|
258 |
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
|
259 |
} |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
260 |
|
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64657
diff
changeset
|
261 |
|
64797 | 262 |
/* blobs */ |
263 |
||
264 |
def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = |
|
265 |
(for { |
|
266 |
(node_name, node) <- nodes.iterator |
|
65361 | 267 |
if !session_base.loaded_theory(node_name) |
64797 | 268 |
cmd <- node.load_commands.iterator |
269 |
name <- cmd.blobs_undefined.iterator |
|
270 |
} yield name).toList |
|
271 |
||
272 |
||
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
273 |
/* document changes */ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
50415
diff
changeset
|
274 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56315
diff
changeset
|
275 |
def parse_change( |
56315 | 276 |
reparse_limit: Int, |
277 |
previous: Document.Version, |
|
278 |
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
|
279 |
edits: List[Document.Edit_Text], |
70796
2739631ac368
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
wenzelm
parents:
70740
diff
changeset
|
280 |
consolidate: List[Document.Node.Name]): Session.Change = |
2739631ac368
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
wenzelm
parents:
70740
diff
changeset
|
281 |
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
|
282 |
|
73340 | 283 |
def commit(change: Session.Change): Unit = {} |
66959 | 284 |
|
285 |
||
286 |
/* theory and file dependencies */ |
|
287 |
||
69007 | 288 |
def dependencies( |
289 |
thys: List[(Document.Node.Name, Position.T)], |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
70796
diff
changeset
|
290 |
progress: Progress = new Progress): Dependencies[Unit] = |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
291 |
Dependencies.empty[Unit].require_thys((), thys, progress = progress) |
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
292 |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
70796
diff
changeset
|
293 |
def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
294 |
: Dependencies[Options] = |
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
295 |
{ |
73359 | 296 |
info.theories.foldLeft(Dependencies.empty[Options]) { |
297 |
case (dependencies, (options, thys)) => |
|
298 |
dependencies.require_thys(options, |
|
299 |
for { (thy, pos) <- thys } yield (import_name(info, thy), pos), |
|
300 |
progress = progress) |
|
301 |
} |
|
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
302 |
} |
69007 | 303 |
|
66959 | 304 |
object Dependencies |
305 |
{ |
|
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
306 |
def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty) |
69007 | 307 |
|
308 |
private def show_path(names: List[Document.Node.Name]): String = |
|
309 |
names.map(name => quote(name.theory)).mkString(" via ") |
|
310 |
||
311 |
private def cycle_msg(names: List[Document.Node.Name]): String = |
|
312 |
"Cyclic dependency of " + show_path(names) |
|
313 |
||
314 |
private def required_by(initiators: List[Document.Node.Name]): String = |
|
315 |
if (initiators.isEmpty) "" |
|
316 |
else "\n(required by " + show_path(initiators.reverse) + ")" |
|
66959 | 317 |
} |
318 |
||
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
319 |
final class Dependencies[A] private( |
66959 | 320 |
rev_entries: List[Document.Node.Entry], |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
321 |
seen: Map[Document.Node.Name, A]) |
66959 | 322 |
{ |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
323 |
private def cons(entry: Document.Node.Entry): Dependencies[A] = |
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
324 |
new Dependencies[A](entry :: rev_entries, seen) |
66959 | 325 |
|
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
326 |
def require_thy(adjunct: A, |
69007 | 327 |
thy: (Document.Node.Name, Position.T), |
328 |
initiators: List[Document.Node.Name] = Nil, |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
70796
diff
changeset
|
329 |
progress: Progress = new Progress): Dependencies[A] = |
69007 | 330 |
{ |
331 |
val (name, pos) = thy |
|
332 |
||
333 |
def message: String = |
|
334 |
"The error(s) above occurred for theory " + quote(name.theory) + |
|
335 |
Dependencies.required_by(initiators) + Position.here(pos) |
|
336 |
||
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
337 |
if (seen.isDefinedAt(name)) this |
69007 | 338 |
else { |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
339 |
val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct)) |
69007 | 340 |
if (session_base.loaded_theory(name)) dependencies1 |
341 |
else { |
|
342 |
try { |
|
343 |
if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators)) |
|
344 |
||
345 |
progress.expose_interrupt() |
|
346 |
val header = |
|
72772 | 347 |
try { |
72777
164cb0806d0a
proper positions for inlined command messages, e.g. for completion within theory header;
wenzelm
parents:
72776
diff
changeset
|
348 |
with_thy_reader(name, check_thy(name, _, command = false)).cat_errors(message) |
72772 | 349 |
} |
69007 | 350 |
catch { case ERROR(msg) => cat_error(msg, message) } |
351 |
val entry = Document.Node.Entry(name, header) |
|
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
70634
diff
changeset
|
352 |
dependencies1.require_thys(adjunct, header.imports_pos, |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
353 |
initiators = name :: initiators, progress = progress).cons(entry) |
69007 | 354 |
} |
355 |
catch { |
|
356 |
case e: Throwable => |
|
357 |
dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e)))) |
|
358 |
} |
|
359 |
} |
|
360 |
} |
|
361 |
} |
|
362 |
||
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
363 |
def require_thys(adjunct: A, |
69007 | 364 |
thys: List[(Document.Node.Name, Position.T)], |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
70796
diff
changeset
|
365 |
progress: Progress = new Progress, |
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
366 |
initiators: List[Document.Node.Name] = Nil): Dependencies[A] = |
73359 | 367 |
thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) |
66959 | 368 |
|
369 |
def entries: List[Document.Node.Entry] = rev_entries.reverse |
|
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
370 |
|
67059 | 371 |
def theories: List[Document.Node.Name] = entries.map(_.name) |
72062 | 372 |
def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name))) |
66959 | 373 |
|
374 |
def errors: List[String] = entries.flatMap(_.header.errors) |
|
375 |
||
69008
d55783ea6cf6
more detailed session dependencies, with conditions for theories;
wenzelm
parents:
69007
diff
changeset
|
376 |
def check_errors: Dependencies[A] = |
67056 | 377 |
errors match { |
378 |
case Nil => this |
|
379 |
case errs => error(cat_lines(errs)) |
|
380 |
} |
|
381 |
||
70674
29bb1ebb188f
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents:
70673
diff
changeset
|
382 |
lazy val theory_graph: Document.Node.Name.Graph[Unit] = |
70652 | 383 |
{ |
384 |
val regular = theories.toSet |
|
385 |
val irregular = |
|
386 |
(for { |
|
387 |
entry <- entries.iterator |
|
388 |
imp <- entry.header.imports |
|
389 |
if !regular(imp) |
|
390 |
} yield imp).toSet |
|
391 |
||
70674
29bb1ebb188f
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents:
70673
diff
changeset
|
392 |
Document.Node.Name.make_graph( |
70652 | 393 |
irregular.toList.map(name => ((name, ()), Nil)) ::: |
394 |
entries.map(entry => ((entry.name, ()), entry.header.imports))) |
|
395 |
} |
|
70650 | 396 |
|
66959 | 397 |
lazy val loaded_theories: Graph[String, Outer_Syntax] = |
73359 | 398 |
entries.foldLeft(session_base.loaded_theories) { |
399 |
case (graph, entry) => |
|
400 |
val name = entry.name.theory |
|
401 |
val imports = entry.header.imports.map(_.theory) |
|
66959 | 402 |
|
73359 | 403 |
val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty)) |
404 |
val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name)) |
|
66959 | 405 |
|
73359 | 406 |
val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil |
407 |
val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) |
|
408 |
val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header |
|
409 |
||
410 |
graph2.map_node(name, _ => syntax) |
|
411 |
} |
|
66959 | 412 |
|
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
413 |
def get_syntax(name: Document.Node.Name): Outer_Syntax = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
414 |
loaded_theories.get_node(name.theory) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
415 |
|
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
416 |
def load_commands: List[(Document.Node.Name, List[Command_Span.Span])] = |
72799 | 417 |
theories.zip( |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
418 |
Par_List.map((e: () => List[Command_Span.Span]) => e(), |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
419 |
theories.map(name => resources.load_commands(get_syntax(name), name)))) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
420 |
.filter(p => p._2.nonEmpty) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
421 |
|
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
422 |
def loaded_files(name: Document.Node.Name, spans: List[Command_Span.Span]) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
423 |
: (String, List[Path]) = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
424 |
{ |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
425 |
val theory = name.theory |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
426 |
val syntax = get_syntax(name) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
427 |
val files1 = resources.loaded_files(syntax, name, spans) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
428 |
val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
429 |
(theory, files1 ::: files2) |
66959 | 430 |
} |
431 |
||
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
432 |
def loaded_files: List[Path] = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
433 |
for { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
434 |
(name, spans) <- load_commands |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
435 |
file <- loaded_files(name, spans)._2 |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
436 |
} yield file |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
437 |
|
66959 | 438 |
def imported_files: List[Path] = |
439 |
{ |
|
440 |
val base_theories = |
|
67059 | 441 |
loaded_theories.all_preds(theories.map(_.theory)). |
72063 | 442 |
filter(session_base.loaded_theories.defined) |
66959 | 443 |
|
70740 | 444 |
base_theories.map(theory => session_base.known_theories(theory).name.path) ::: |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72799
diff
changeset
|
445 |
base_theories.flatMap(session_base.known_loaded_files.withDefaultValue(Nil)) |
66959 | 446 |
} |
447 |
||
448 |
lazy val overall_syntax: Outer_Syntax = |
|
72063 | 449 |
Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node)) |
66959 | 450 |
|
451 |
override def toString: String = entries.toString |
|
452 |
} |
|
43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
diff
changeset
|
453 |
} |