author | wenzelm |
Thu, 22 Mar 2018 17:05:06 +0100 | |
changeset 67925 | 74dce5658d4c |
parent 67923 | 3e072441c96a |
child 67936 | 141a93b93aa6 |
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 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
89 |
def use_theories( |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
90 |
theories: List[(String, Position.T)], |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
91 |
qualifier: String = Sessions.DRAFT, |
67881 | 92 |
master_dir: String = "", |
67885 | 93 |
id: UUID = UUID(), |
67881 | 94 |
progress: Progress = No_Progress): Theories_Result = |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
95 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
96 |
val dep_theories = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
97 |
resources.load_theories(session, id, theories, qualifier = qualifier, |
67881 | 98 |
master_dir = master_dir, progress = progress) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
99 |
|
67879 | 100 |
val result = Future.promise[Theories_Result] |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
101 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
102 |
def check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
103 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
104 |
val state = session.current_state() |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
105 |
state.stable_tip_version match { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
106 |
case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) => |
67889 | 107 |
val nodes = |
108 |
for (name <- dep_theories) |
|
109 |
yield (name -> Protocol.node_status(state, version, name, version.nodes(name))) |
|
110 |
try { result.fulfill(Theories_Result(state, version, nodes)) } |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
111 |
catch { case _: IllegalStateException => } |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
112 |
case _ => |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
113 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
114 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
115 |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
116 |
val check_progress = |
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
117 |
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
|
118 |
{ 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
|
119 |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
120 |
val consumer = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
121 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
122 |
case changed => if (dep_theories.exists(changed.nodes)) check_state |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
123 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
124 |
|
67892 | 125 |
try { |
126 |
session.commands_changed += consumer |
|
127 |
result.join_result |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
128 |
check_progress.cancel |
67892 | 129 |
session.commands_changed -= consumer |
130 |
} |
|
131 |
finally { |
|
132 |
resources.unload_theories(session, id, dep_theories) |
|
133 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
134 |
|
67879 | 135 |
result.join |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
136 |
} |
67063 | 137 |
} |
138 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
139 |
|
67054 | 140 |
/* internal state */ |
141 |
||
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
142 |
sealed case class State( |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
143 |
required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
144 |
theories: Map[Document.Node.Name, Theory] = Map.empty) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
145 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
146 |
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
147 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
148 |
def insert_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
149 |
copy(required = (required /: names)(_.insert(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
150 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
151 |
def remove_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
152 |
copy(required = (required /: names)(_.remove(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
153 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
154 |
def update_theories(update: List[(Document.Node.Name, Theory)]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
155 |
copy(theories = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
156 |
(theories /: update)({ case (thys, (name, thy)) => |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
157 |
thys.get(name) match { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
158 |
case Some(thy1) if thy1 == thy => thys |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
159 |
case _ => thys + (name -> thy) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
160 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
161 |
})) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
162 |
} |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
163 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
164 |
final class Theory private[Thy_Resources]( |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
165 |
val node_name: Document.Node.Name, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
166 |
val node_header: Document.Node.Header, |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
167 |
val text: String, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
168 |
val node_required: Boolean) |
67056 | 169 |
{ |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
170 |
override def toString: String = node_name.toString |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
171 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
172 |
def node_perspective: Document.Node.Perspective_Text = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
173 |
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
|
174 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
175 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
176 |
{ |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
177 |
val (text_edits, old_required) = |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
178 |
if (old.isEmpty) (Text.Edit.inserts(0, text), false) |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
179 |
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
|
180 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
181 |
if (text_edits.isEmpty && node_required == old_required) Nil |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
182 |
else |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
183 |
List(node_name -> Document.Node.Deps(node_header), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
184 |
node_name -> Document.Node.Edits(text_edits), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
185 |
node_name -> node_perspective) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
186 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
187 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
188 |
def required(required: Boolean): Theory = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
189 |
if (required == node_required) this |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
190 |
else new Theory(node_name, node_header, text, required) |
67056 | 191 |
} |
67054 | 192 |
} |
193 |
||
67056 | 194 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 195 |
extends Resources(session_base, log = log) |
196 |
{ |
|
67056 | 197 |
resources => |
198 |
||
67054 | 199 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 200 |
|
201 |
def load_theories( |
|
202 |
session: Session, |
|
67885 | 203 |
id: UUID, |
67056 | 204 |
theories: List[(String, Position.T)], |
205 |
qualifier: String = Sessions.DRAFT, |
|
67881 | 206 |
master_dir: String = "", |
207 |
progress: Progress = No_Progress): List[Document.Node.Name] = |
|
67056 | 208 |
{ |
209 |
val import_names = |
|
210 |
for ((thy, pos) <- theories) |
|
211 |
yield (import_name(qualifier, master_dir, thy), pos) |
|
212 |
||
67881 | 213 |
val dependencies = resources.dependencies(import_names, progress = progress).check_errors |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
214 |
val dep_theories = dependencies.theories |
67888 | 215 |
|
216 |
val loaded_theories = |
|
217 |
for (node_name <- dep_theories) |
|
218 |
yield { |
|
219 |
val path = node_name.path |
|
220 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
|
221 |
||
222 |
progress.expose_interrupt() |
|
223 |
val text = File.read(path) |
|
224 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
|
225 |
new Thy_Resources.Theory(node_name, node_header, text, true) |
|
226 |
} |
|
67056 | 227 |
|
67893 | 228 |
state.change(st => |
229 |
{ |
|
230 |
val st1 = st.insert_required(id, dep_theories) |
|
231 |
val theory_edits = |
|
232 |
for (theory <- loaded_theories) |
|
233 |
yield { |
|
234 |
val node_name = theory.node_name |
|
235 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
236 |
val edits = theory1.node_edits(st1.theories.get(node_name)) |
|
237 |
(edits, (node_name, theory1)) |
|
238 |
} |
|
239 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
240 |
st1.update_theories(theory_edits.map(_._2)) |
|
241 |
}) |
|
67056 | 242 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
243 |
dep_theories |
67056 | 244 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
245 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
246 |
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
|
247 |
{ |
67893 | 248 |
state.change(st => |
249 |
{ |
|
250 |
val st1 = st.remove_required(id, dep_theories) |
|
251 |
val theory_edits = |
|
252 |
for { |
|
253 |
node_name <- dep_theories |
|
254 |
theory <- st1.theories.get(node_name) |
|
255 |
} |
|
256 |
yield { |
|
257 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
258 |
val edits = theory1.node_edits(Some(theory)) |
|
259 |
(edits, (node_name, theory1)) |
|
260 |
} |
|
261 |
session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) |
|
262 |
st1.update_theories(theory_edits.map(_._2)) |
|
263 |
}) |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
264 |
} |
67054 | 265 |
} |