author | wenzelm |
Fri, 07 Sep 2018 20:35:18 +0200 | |
changeset 68935 | 7a420bee1eea |
parent 68925 | 76ce16eefab9 |
child 68936 | 90c08c7bab9c |
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, |
67948 | 21 |
include_sessions: List[String] = Nil, |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
22 |
session_base: Option[Sessions.Base] = None, |
67869 | 23 |
print_mode: List[String] = Nil, |
24 |
progress: Progress = No_Progress, |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
25 |
log: Logger = No_Logger): Session = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
26 |
{ |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
27 |
val base = |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
28 |
session_base getOrElse |
67948 | 29 |
Sessions.base_info(options, session_name, include_sessions = include_sessions, |
30 |
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
|
31 |
val resources = new Thy_Resources(base, log = log) |
67945 | 32 |
val session = new Session(session_name, options, resources) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
33 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
34 |
val session_error = Future.promise[String] |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
35 |
var session_phase: Session.Consumer[Session.Phase] = null |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
36 |
session_phase = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
37 |
Session.Consumer(getClass.getName) { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
38 |
case Session.Ready => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
39 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
40 |
session_error.fulfill("") |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
41 |
case Session.Terminated(result) if !result.ok => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
42 |
session.phase_changed -= session_phase |
67869 | 43 |
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
|
44 |
case _ => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
45 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
46 |
session.phase_changed += session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
47 |
|
67877 | 48 |
progress.echo("Starting " + session_name + " ...") |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
49 |
Isabelle_Process.start(session, options, |
67869 | 50 |
logic = session_name, dirs = session_dirs, modes = print_mode) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
51 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
52 |
session_error.join match { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
53 |
case "" => session |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
54 |
case msg => session.stop(); error(msg) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
55 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
56 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
57 |
|
68916 | 58 |
private def stable_snapshot( |
59 |
state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = |
|
60 |
{ |
|
61 |
val snapshot = state.snapshot(name) |
|
62 |
assert(version.id == snapshot.version.id) |
|
63 |
snapshot |
|
64 |
} |
|
65 |
||
68365 | 66 |
class Theories_Result private[Thy_Resources]( |
67883 | 67 |
val state: Document.State, |
67889 | 68 |
val version: Document.Version, |
68925 | 69 |
val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], |
70 |
val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) |
|
67879 | 71 |
{ |
68925 | 72 |
def snapshot(name: Document.Node.Name): Document.Snapshot = |
73 |
stable_snapshot(state, version, name) |
|
74 |
||
75 |
def ok: Boolean = |
|
76 |
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
|
67879 | 77 |
} |
78 |
||
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
79 |
val default_check_delay: Double = 0.5 |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
80 |
val default_nodes_status_delay: Double = -1.0 |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
81 |
|
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
82 |
|
67063 | 83 |
class Session private[Thy_Resources]( |
67945 | 84 |
session_name: String, |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
85 |
session_options: Options, |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
86 |
override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) |
67063 | 87 |
{ |
88 |
session => |
|
89 |
||
68922 | 90 |
|
91 |
/* temporary directory */ |
|
92 |
||
67925 | 93 |
val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") |
67946 | 94 |
val tmp_dir_name: String = File.path(tmp_dir).implode |
67925 | 95 |
|
68923 | 96 |
def master_directory(master_dir: String): String = |
97 |
proper_string(master_dir) getOrElse tmp_dir_name |
|
98 |
||
67945 | 99 |
override def toString: String = session_name |
100 |
||
67925 | 101 |
override def stop(): Process_Result = |
102 |
{ |
|
103 |
try { super.stop() } |
|
104 |
finally { Isabelle_System.rm_tree(tmp_dir) } |
|
105 |
} |
|
106 |
||
67936 | 107 |
|
108 |
/* theories */ |
|
109 |
||
68914 | 110 |
private sealed case class Use_Theories_State( |
111 |
last_update: Time = Time.now(), |
|
112 |
nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
|
68916 | 113 |
already_initialized: Set[Document.Node.Name] = Set.empty, |
68925 | 114 |
already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, |
68916 | 115 |
result: Promise[Theories_Result] = Future.promise[Theories_Result]) |
68914 | 116 |
{ |
117 |
def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
|
118 |
copy(last_update = Time.now(), nodes_status = new_nodes_status) |
|
119 |
||
120 |
def watchdog(watchdog_timeout: Time): Boolean = |
|
121 |
watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
|
122 |
||
123 |
def initialized_theories( |
|
124 |
state: Document.State, |
|
125 |
version: Document.Version, |
|
68916 | 126 |
theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) = |
68914 | 127 |
{ |
128 |
val initialized = |
|
129 |
for { |
|
68916 | 130 |
name <- theories |
68914 | 131 |
if !already_initialized(name) && |
132 |
Document_Status.Node_Status.make(state, version, name).initialized |
|
133 |
} yield name |
|
134 |
(initialized, copy(already_initialized = already_initialized ++ initialized)) |
|
135 |
} |
|
68916 | 136 |
|
137 |
def cancel_result { result.cancel } |
|
138 |
def await_result { result.join_result } |
|
139 |
def join_result: Theories_Result = result.join |
|
140 |
def check_result( |
|
141 |
state: Document.State, |
|
142 |
version: Document.Version, |
|
68925 | 143 |
dep_theories: List[Document.Node.Name], |
68916 | 144 |
beyond_limit: Boolean, |
145 |
watchdog_timeout: Time, |
|
146 |
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit]) |
|
147 |
: Use_Theories_State = |
|
148 |
{ |
|
149 |
val st1 = |
|
150 |
if (commit.isDefined) { |
|
151 |
val committed = |
|
152 |
for { |
|
68925 | 153 |
name <- dep_theories |
154 |
if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name) |
|
68916 | 155 |
} |
156 |
yield { |
|
157 |
val snapshot = stable_snapshot(state, version, name) |
|
158 |
val status = Document_Status.Node_Status.make(state, version, name) |
|
159 |
commit.get.apply(snapshot, status) |
|
68925 | 160 |
(name -> status) |
68916 | 161 |
} |
162 |
copy(already_committed = already_committed ++ committed) |
|
163 |
} |
|
164 |
else this |
|
165 |
||
166 |
if (beyond_limit || watchdog(watchdog_timeout) || |
|
68925 | 167 |
dep_theories.forall(name => |
168 |
already_committed.isDefinedAt(name) || |
|
68916 | 169 |
state.node_consolidated(version, name) || |
170 |
nodes_status.quasi_consolidated(name))) |
|
171 |
{ |
|
172 |
val nodes = |
|
68925 | 173 |
for (name <- dep_theories) |
68916 | 174 |
yield { (name -> Document_Status.Node_Status.make(state, version, name)) } |
68925 | 175 |
val nodes_committed = |
176 |
for { |
|
177 |
name <- dep_theories |
|
178 |
status <- already_committed.get(name) |
|
179 |
} yield (name -> status) |
|
180 |
||
181 |
try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) } |
|
68916 | 182 |
catch { case _: IllegalStateException => } |
183 |
} |
|
184 |
||
185 |
st1 |
|
186 |
} |
|
68914 | 187 |
} |
188 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
189 |
def use_theories( |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67939
diff
changeset
|
190 |
theories: List[String], |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
191 |
qualifier: String = Sessions.DRAFT, |
67881 | 192 |
master_dir: String = "", |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
193 |
check_delay: Time = Time.seconds(default_check_delay), |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
194 |
check_limit: Int = 0, |
68908 | 195 |
watchdog_timeout: Time = Time.zero, |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
196 |
nodes_status_delay: Time = Time.seconds(default_nodes_status_delay), |
67885 | 197 |
id: UUID = UUID(), |
68916 | 198 |
// commit: must not block, must not fail |
199 |
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, |
|
67881 | 200 |
progress: Progress = No_Progress): Theories_Result = |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
201 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
202 |
val dep_theories = |
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
203 |
{ |
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
204 |
val import_names = |
68923 | 205 |
theories.map(thy => |
206 |
resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) |
|
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
207 |
resources.dependencies(import_names, progress = progress).check_errors.theories |
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
208 |
} |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
209 |
val dep_theories_set = dep_theories.toSet |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
210 |
|
68914 | 211 |
val use_theories_state = Synchronized(Use_Theories_State()) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
212 |
|
68916 | 213 |
def check_result(beyond_limit: Boolean = false) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
214 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
215 |
val state = session.current_state() |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
216 |
state.stable_tip_version match { |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
217 |
case Some(version) => |
68916 | 218 |
use_theories_state.change( |
219 |
_.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit)) |
|
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
220 |
case None => |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
221 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
222 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
223 |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
224 |
val check_progress = |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
225 |
{ |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
226 |
var check_count = 0 |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
227 |
Event_Timer.request(Time.now(), repeat = Some(check_delay)) |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
228 |
{ |
68916 | 229 |
if (progress.stopped) use_theories_state.value.cancel_result |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
230 |
else { |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
231 |
check_count += 1 |
68916 | 232 |
check_result(check_limit > 0 && check_count > check_limit) |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
233 |
} |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
234 |
} |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
235 |
} |
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
236 |
|
68906 | 237 |
val consumer = |
238 |
{ |
|
239 |
val delay_nodes_status = |
|
240 |
Standard_Thread.delay_first(nodes_status_delay max Time.zero) { |
|
68914 | 241 |
progress.nodes_status(use_theories_state.value.nodes_status) |
68906 | 242 |
} |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
243 |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
244 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
68330 | 245 |
case changed => |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
246 |
if (changed.nodes.exists(dep_theories_set)) { |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
247 |
val snapshot = session.snapshot() |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
248 |
val state = snapshot.state |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
249 |
val version = snapshot.version |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
250 |
|
68903 | 251 |
val theory_percentages = |
68914 | 252 |
use_theories_state.change_result(st => |
68903 | 253 |
{ |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
254 |
val domain = |
68914 | 255 |
if (st.nodes_status.is_empty) dep_theories_set |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
256 |
else changed.nodes.iterator.filter(dep_theories_set).toSet |
68899 | 257 |
|
68903 | 258 |
val (nodes_status_changed, nodes_status1) = |
68914 | 259 |
st.nodes_status.update(resources.session_base, state, version, |
68903 | 260 |
domain = Some(domain), trim = changed.assignment) |
68899 | 261 |
|
68903 | 262 |
if (nodes_status_delay >= Time.zero && nodes_status_changed) { |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
263 |
delay_nodes_status.invoke |
68899 | 264 |
} |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
265 |
|
68903 | 266 |
val progress_percentage = |
68905 | 267 |
(for { |
68904 | 268 |
(name, node_status) <- nodes_status1.present.iterator |
68903 | 269 |
if changed.nodes.contains(name) |
270 |
p1 = node_status.percentage |
|
68914 | 271 |
if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage) |
68905 | 272 |
} yield (name.theory, p1)).toList |
68903 | 273 |
|
68914 | 274 |
(progress_percentage, st.update(nodes_status1)) |
68903 | 275 |
}) |
68330 | 276 |
|
277 |
val check_theories = |
|
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
278 |
(for { |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
279 |
command <- changed.commands.iterator |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
280 |
if dep_theories_set(command.node_name) && command.potentially_initialized |
68914 | 281 |
} yield command.node_name).toList |
68330 | 282 |
|
283 |
if (check_theories.nonEmpty) { |
|
284 |
val initialized = |
|
68914 | 285 |
use_theories_state.change_result( |
286 |
_.initialized_theories(state, version, check_theories)) |
|
68330 | 287 |
initialized.map(_.theory).sorted.foreach(progress.theory("", _)) |
288 |
} |
|
289 |
||
68903 | 290 |
for ((theory, percentage) <- theory_percentages) |
291 |
progress.theory_percentage("", theory, percentage) |
|
292 |
||
68916 | 293 |
check_result() |
68330 | 294 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
295 |
} |
68906 | 296 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
297 |
|
67892 | 298 |
try { |
299 |
session.commands_changed += consumer |
|
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
300 |
resources.load_theories(session, id, dep_theories, progress) |
68916 | 301 |
use_theories_state.value.await_result |
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
302 |
check_progress.cancel |
67892 | 303 |
} |
304 |
finally { |
|
68907 | 305 |
session.commands_changed -= consumer |
67892 | 306 |
resources.unload_theories(session, id, dep_theories) |
307 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
308 |
|
68916 | 309 |
use_theories_state.value.join_result |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
310 |
} |
67936 | 311 |
|
67939 | 312 |
def purge_theories( |
68915 | 313 |
theories: List[String], |
314 |
qualifier: String = Sessions.DRAFT, |
|
315 |
master_dir: String = "", |
|
316 |
all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = |
|
317 |
{ |
|
68923 | 318 |
val nodes = |
319 |
if (all) None |
|
320 |
else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) |
|
68915 | 321 |
resources.purge_theories(session, nodes) |
322 |
} |
|
67063 | 323 |
} |
324 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
325 |
|
67054 | 326 |
/* internal state */ |
327 |
||
68922 | 328 |
final class Theory private[Thy_Resources]( |
329 |
val node_name: Document.Node.Name, |
|
330 |
val node_header: Document.Node.Header, |
|
331 |
val text: String, |
|
332 |
val node_required: Boolean) |
|
333 |
{ |
|
334 |
override def toString: String = node_name.toString |
|
335 |
||
336 |
def node_perspective: Document.Node.Perspective_Text = |
|
337 |
Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) |
|
338 |
||
339 |
def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = |
|
340 |
List(node_name -> Document.Node.Deps(node_header), |
|
341 |
node_name -> Document.Node.Edits(text_edits), |
|
342 |
node_name -> node_perspective) |
|
343 |
||
344 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
|
345 |
{ |
|
346 |
val (text_edits, old_required) = |
|
347 |
if (old.isEmpty) (Text.Edit.inserts(0, text), false) |
|
348 |
else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) |
|
349 |
||
350 |
if (text_edits.isEmpty && node_required == old_required) Nil |
|
351 |
else make_edits(text_edits) |
|
352 |
} |
|
353 |
||
354 |
def purge_edits: List[Document.Edit_Text] = |
|
355 |
make_edits(Text.Edit.removes(0, text)) |
|
356 |
||
357 |
def required(required: Boolean): Theory = |
|
358 |
if (required == node_required) this |
|
359 |
else new Theory(node_name, node_header, text, required) |
|
360 |
} |
|
361 |
||
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
362 |
sealed case class State( |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
363 |
required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
364 |
theories: Map[Document.Node.Name, Theory] = Map.empty) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
365 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
366 |
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
367 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
368 |
def insert_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
369 |
copy(required = (required /: names)(_.insert(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
370 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
371 |
def remove_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
372 |
copy(required = (required /: names)(_.remove(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
373 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
374 |
def update_theories(update: List[(Document.Node.Name, Theory)]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
375 |
copy(theories = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
376 |
(theories /: update)({ case (thys, (name, thy)) => |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
377 |
thys.get(name) match { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
378 |
case Some(thy1) if thy1 == thy => thys |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
379 |
case _ => thys + (name -> thy) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
380 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
381 |
})) |
67936 | 382 |
|
383 |
def remove_theories(remove: List[Document.Node.Name]): State = |
|
384 |
{ |
|
385 |
require(remove.forall(name => !is_required(name))) |
|
386 |
copy(theories = theories -- remove) |
|
387 |
} |
|
388 |
||
68935 | 389 |
lazy val theory_graph: Graph[Document.Node.Name, Unit] = |
67936 | 390 |
{ |
391 |
val entries = |
|
392 |
for ((name, theory) <- theories.toList) |
|
393 |
yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_))) |
|
394 |
Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering) |
|
395 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
396 |
} |
67054 | 397 |
} |
398 |
||
67056 | 399 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 400 |
extends Resources(session_base, log = log) |
401 |
{ |
|
67056 | 402 |
resources => |
403 |
||
67054 | 404 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 405 |
|
406 |
def load_theories( |
|
407 |
session: Session, |
|
67885 | 408 |
id: UUID, |
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
409 |
dep_theories: List[Document.Node.Name], |
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
410 |
progress: Progress) |
67056 | 411 |
{ |
67888 | 412 |
|
413 |
val loaded_theories = |
|
414 |
for (node_name <- dep_theories) |
|
415 |
yield { |
|
416 |
val path = node_name.path |
|
417 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
|
418 |
||
419 |
progress.expose_interrupt() |
|
420 |
val text = File.read(path) |
|
421 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
|
422 |
new Thy_Resources.Theory(node_name, node_header, text, true) |
|
423 |
} |
|
67056 | 424 |
|
67893 | 425 |
state.change(st => |
426 |
{ |
|
427 |
val st1 = st.insert_required(id, dep_theories) |
|
428 |
val theory_edits = |
|
429 |
for (theory <- loaded_theories) |
|
430 |
yield { |
|
431 |
val node_name = theory.node_name |
|
432 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
433 |
val edits = theory1.node_edits(st1.theories.get(node_name)) |
|
434 |
(edits, (node_name, theory1)) |
|
435 |
} |
|
436 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
437 |
st1.update_theories(theory_edits.map(_._2)) |
|
438 |
}) |
|
67056 | 439 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
440 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
441 |
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
|
442 |
{ |
67893 | 443 |
state.change(st => |
444 |
{ |
|
445 |
val st1 = st.remove_required(id, dep_theories) |
|
446 |
val theory_edits = |
|
447 |
for { |
|
448 |
node_name <- dep_theories |
|
449 |
theory <- st1.theories.get(node_name) |
|
450 |
} |
|
451 |
yield { |
|
452 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
453 |
val edits = theory1.node_edits(Some(theory)) |
|
454 |
(edits, (node_name, theory1)) |
|
455 |
} |
|
456 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
457 |
st1.update_theories(theory_edits.map(_._2)) |
|
458 |
}) |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
459 |
} |
67936 | 460 |
|
68915 | 461 |
def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
462 |
: (List[Document.Node.Name], List[Document.Node.Name]) = |
|
67936 | 463 |
{ |
464 |
state.change_result(st => |
|
465 |
{ |
|
68935 | 466 |
val graph = st.theory_graph |
67936 | 467 |
val all_nodes = graph.topological_order |
468 |
||
469 |
val purge = |
|
68915 | 470 |
(if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))). |
67936 | 471 |
filterNot(st.is_required(_)).toSet |
67943 | 472 |
|
473 |
val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet |
|
474 |
val (retained, purged) = all_nodes.partition(retain) |
|
67936 | 475 |
|
476 |
val purge_edits = purged.flatMap(name => st.theories(name).purge_edits) |
|
477 |
session.update(Document.Blobs.empty, purge_edits) |
|
478 |
||
67943 | 479 |
((purged, retained), st.remove_theories(purged)) |
67936 | 480 |
}) |
481 |
} |
|
67054 | 482 |
} |