author | wenzelm |
Fri, 23 Mar 2018 22:44:43 +0100 | |
changeset 67939 | 544a7a21298e |
parent 67936 | 141a93b93aa6 |
child 67940 | b4e80f062fbf |
permissions | -rw-r--r-- |
67054 | 1 |
/* Title: Pure/Thy/thy_resources.scala |
2 |
Author: Makarius |
|
3 |
||
67892 | 4 |
PIDE resources for theory files: load/unload theories via PIDE document updates. |
67054 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67925 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
67054 | 13 |
object Thy_Resources |
14 |
{ |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
15 |
/* PIDE session */ |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
16 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
17 |
def start_session( |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
18 |
options: Options, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
19 |
session_name: String, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
20 |
session_dirs: List[Path] = Nil, |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
21 |
session_base: Option[Sessions.Base] = None, |
67869 | 22 |
print_mode: List[String] = Nil, |
23 |
progress: Progress = No_Progress, |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
24 |
log: Logger = No_Logger): Session = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
25 |
{ |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
26 |
val base = |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
27 |
session_base getOrElse |
67852
f701a1d5d852
allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
wenzelm
parents:
67064
diff
changeset
|
28 |
Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
29 |
val resources = new Thy_Resources(base, log = log) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
30 |
val session = new Session(options, resources) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
31 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
32 |
val session_error = Future.promise[String] |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
33 |
var session_phase: Session.Consumer[Session.Phase] = null |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
34 |
session_phase = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
35 |
Session.Consumer(getClass.getName) { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
36 |
case Session.Ready => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
37 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
38 |
session_error.fulfill("") |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
39 |
case Session.Terminated(result) if !result.ok => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
40 |
session.phase_changed -= session_phase |
67869 | 41 |
session_error.fulfill("Session start failed: return code " + result.rc) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
42 |
case _ => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
43 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
44 |
session.phase_changed += session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
45 |
|
67877 | 46 |
progress.echo("Starting " + session_name + " ...") |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
47 |
Isabelle_Process.start(session, options, |
67869 | 48 |
logic = session_name, dirs = session_dirs, modes = print_mode) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
49 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
50 |
session_error.join match { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
51 |
case "" => session |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
52 |
case msg => session.stop(); error(msg) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
53 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
54 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
55 |
|
67879 | 56 |
sealed case class Theories_Result( |
67883 | 57 |
val state: Document.State, |
67889 | 58 |
val version: Document.Version, |
59 |
val nodes: List[(Document.Node.Name, Protocol.Node_Status)]) |
|
67879 | 60 |
{ |
67883 | 61 |
def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) |
67897 | 62 |
|
63 |
def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] = |
|
64 |
{ |
|
65 |
val node = version.nodes(node_name) |
|
66 |
(for { |
|
67 |
(command, start) <- |
|
68 |
Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node)) |
|
69 |
pos = command.span.keyword_pos(start).position(command.span.name) |
|
70 |
(_, tree) <- state.command_results(version, command).iterator |
|
71 |
} yield (tree, pos)).toList |
|
72 |
} |
|
67879 | 73 |
} |
74 |
||
67063 | 75 |
class Session private[Thy_Resources]( |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
76 |
session_options: Options, |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
77 |
override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) |
67063 | 78 |
{ |
79 |
session => |
|
80 |
||
67925 | 81 |
val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") |
82 |
||
83 |
override def stop(): Process_Result = |
|
84 |
{ |
|
85 |
try { super.stop() } |
|
86 |
finally { Isabelle_System.rm_tree(tmp_dir) } |
|
87 |
} |
|
88 |
||
67936 | 89 |
|
90 |
/* theories */ |
|
91 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
92 |
def use_theories( |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
93 |
theories: List[(String, Position.T)], |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
94 |
qualifier: String = Sessions.DRAFT, |
67881 | 95 |
master_dir: String = "", |
67885 | 96 |
id: UUID = UUID(), |
67881 | 97 |
progress: Progress = No_Progress): Theories_Result = |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
98 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
99 |
val dep_theories = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
100 |
resources.load_theories(session, id, theories, qualifier = qualifier, |
67881 | 101 |
master_dir = master_dir, progress = progress) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
102 |
|
67879 | 103 |
val result = Future.promise[Theories_Result] |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
104 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
105 |
def check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
106 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
107 |
val state = session.current_state() |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
108 |
state.stable_tip_version match { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
109 |
case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) => |
67889 | 110 |
val nodes = |
111 |
for (name <- dep_theories) |
|
112 |
yield (name -> Protocol.node_status(state, version, name, version.nodes(name))) |
|
113 |
try { result.fulfill(Theories_Result(state, version, nodes)) } |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
114 |
catch { case _: IllegalStateException => } |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
115 |
case _ => |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
116 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
117 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
118 |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
119 |
val check_progress = |
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
120 |
Event_Timer.request(Time.now(), repeat = Some(Time.seconds(0.5))) |
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
121 |
{ if (progress.stopped) result.cancel else check_state } |
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
122 |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
123 |
val consumer = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
124 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
125 |
case changed => if (dep_theories.exists(changed.nodes)) check_state |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
126 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
127 |
|
67892 | 128 |
try { |
129 |
session.commands_changed += consumer |
|
130 |
result.join_result |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
131 |
check_progress.cancel |
67892 | 132 |
session.commands_changed -= consumer |
133 |
} |
|
134 |
finally { |
|
135 |
resources.unload_theories(session, id, dep_theories) |
|
136 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
137 |
|
67879 | 138 |
result.join |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
139 |
} |
67936 | 140 |
|
67939 | 141 |
def purge_theories( |
142 |
theories: List[String], |
|
143 |
qualifier: String = Sessions.DRAFT, |
|
144 |
master_dir: String = "", |
|
145 |
all: Boolean = false): List[Document.Node.Name] = |
|
146 |
resources.purge_theories(session, theories = theories, qualifier = qualifier, |
|
147 |
master_dir = master_dir, all = all) |
|
67063 | 148 |
} |
149 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
150 |
|
67054 | 151 |
/* internal state */ |
152 |
||
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
153 |
sealed case class State( |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
154 |
required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
155 |
theories: Map[Document.Node.Name, Theory] = Map.empty) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
156 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
157 |
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
158 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
159 |
def insert_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
160 |
copy(required = (required /: names)(_.insert(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
161 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
162 |
def remove_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
163 |
copy(required = (required /: names)(_.remove(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
164 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
165 |
def update_theories(update: List[(Document.Node.Name, Theory)]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
166 |
copy(theories = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
167 |
(theories /: update)({ case (thys, (name, thy)) => |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
168 |
thys.get(name) match { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
169 |
case Some(thy1) if thy1 == thy => thys |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
170 |
case _ => thys + (name -> thy) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
171 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
172 |
})) |
67936 | 173 |
|
174 |
def remove_theories(remove: List[Document.Node.Name]): State = |
|
175 |
{ |
|
176 |
require(remove.forall(name => !is_required(name))) |
|
177 |
copy(theories = theories -- remove) |
|
178 |
} |
|
179 |
||
180 |
lazy val theories_graph: Graph[Document.Node.Name, Unit] = |
|
181 |
{ |
|
182 |
val entries = |
|
183 |
for ((name, theory) <- theories.toList) |
|
184 |
yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_))) |
|
185 |
Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering) |
|
186 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
187 |
} |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
188 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
189 |
final class Theory private[Thy_Resources]( |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
190 |
val node_name: Document.Node.Name, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
191 |
val node_header: Document.Node.Header, |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
192 |
val text: String, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
193 |
val node_required: Boolean) |
67056 | 194 |
{ |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
195 |
override def toString: String = node_name.toString |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
196 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
197 |
def node_perspective: Document.Node.Perspective_Text = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
198 |
Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
199 |
|
67936 | 200 |
def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = |
201 |
List(node_name -> Document.Node.Deps(node_header), |
|
202 |
node_name -> Document.Node.Edits(text_edits), |
|
203 |
node_name -> node_perspective) |
|
204 |
||
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
205 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
206 |
{ |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
207 |
val (text_edits, old_required) = |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
208 |
if (old.isEmpty) (Text.Edit.inserts(0, text), false) |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
209 |
else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
210 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
211 |
if (text_edits.isEmpty && node_required == old_required) Nil |
67936 | 212 |
else make_edits(text_edits) |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
213 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
214 |
|
67936 | 215 |
def purge_edits: List[Document.Edit_Text] = |
216 |
make_edits(Text.Edit.removes(0, text)) |
|
217 |
||
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
218 |
def required(required: Boolean): Theory = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
219 |
if (required == node_required) this |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
220 |
else new Theory(node_name, node_header, text, required) |
67056 | 221 |
} |
67054 | 222 |
} |
223 |
||
67056 | 224 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 225 |
extends Resources(session_base, log = log) |
226 |
{ |
|
67056 | 227 |
resources => |
228 |
||
67054 | 229 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 230 |
|
231 |
def load_theories( |
|
232 |
session: Session, |
|
67885 | 233 |
id: UUID, |
67056 | 234 |
theories: List[(String, Position.T)], |
235 |
qualifier: String = Sessions.DRAFT, |
|
67881 | 236 |
master_dir: String = "", |
237 |
progress: Progress = No_Progress): List[Document.Node.Name] = |
|
67056 | 238 |
{ |
239 |
val import_names = |
|
240 |
for ((thy, pos) <- theories) |
|
241 |
yield (import_name(qualifier, master_dir, thy), pos) |
|
242 |
||
67881 | 243 |
val dependencies = resources.dependencies(import_names, progress = progress).check_errors |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
244 |
val dep_theories = dependencies.theories |
67888 | 245 |
|
246 |
val loaded_theories = |
|
247 |
for (node_name <- dep_theories) |
|
248 |
yield { |
|
249 |
val path = node_name.path |
|
250 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
|
251 |
||
252 |
progress.expose_interrupt() |
|
253 |
val text = File.read(path) |
|
254 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
|
255 |
new Thy_Resources.Theory(node_name, node_header, text, true) |
|
256 |
} |
|
67056 | 257 |
|
67893 | 258 |
state.change(st => |
259 |
{ |
|
260 |
val st1 = st.insert_required(id, dep_theories) |
|
261 |
val theory_edits = |
|
262 |
for (theory <- loaded_theories) |
|
263 |
yield { |
|
264 |
val node_name = theory.node_name |
|
265 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
266 |
val edits = theory1.node_edits(st1.theories.get(node_name)) |
|
267 |
(edits, (node_name, theory1)) |
|
268 |
} |
|
269 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
270 |
st1.update_theories(theory_edits.map(_._2)) |
|
271 |
}) |
|
67056 | 272 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
273 |
dep_theories |
67056 | 274 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
275 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
276 |
def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
277 |
{ |
67893 | 278 |
state.change(st => |
279 |
{ |
|
280 |
val st1 = st.remove_required(id, dep_theories) |
|
281 |
val theory_edits = |
|
282 |
for { |
|
283 |
node_name <- dep_theories |
|
284 |
theory <- st1.theories.get(node_name) |
|
285 |
} |
|
286 |
yield { |
|
287 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
288 |
val edits = theory1.node_edits(Some(theory)) |
|
289 |
(edits, (node_name, theory1)) |
|
290 |
} |
|
291 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
292 |
st1.update_theories(theory_edits.map(_._2)) |
|
293 |
}) |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
294 |
} |
67936 | 295 |
|
67939 | 296 |
def purge_theories(session: Session, |
297 |
theories: List[String], |
|
298 |
qualifier: String = Sessions.DRAFT, |
|
299 |
master_dir: String = "", |
|
300 |
all: Boolean = false): List[Document.Node.Name] = |
|
67936 | 301 |
{ |
67939 | 302 |
val nodes = theories.map(import_name(qualifier, master_dir, _)) |
303 |
||
67936 | 304 |
state.change_result(st => |
305 |
{ |
|
306 |
val graph = st.theories_graph |
|
307 |
val all_nodes = graph.topological_order |
|
308 |
||
309 |
val purge = |
|
67939 | 310 |
(if (all) all_nodes else nodes.filter(graph.defined(_))). |
67936 | 311 |
filterNot(st.is_required(_)).toSet |
312 |
val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet) |
|
313 |
||
314 |
val purge_edits = purged.flatMap(name => st.theories(name).purge_edits) |
|
315 |
session.update(Document.Blobs.empty, purge_edits) |
|
316 |
||
317 |
(purged, st.remove_theories(purged)) |
|
318 |
}) |
|
319 |
} |
|
67054 | 320 |
} |