author | wenzelm |
Sat, 17 Mar 2018 16:18:05 +0100 | |
changeset 67888 | 3bf62a6e50e7 |
parent 67887 | a4d5342898b1 |
child 67889 | 5c438b774b4d |
permissions | -rw-r--r-- |
67054 | 1 |
/* Title: Pure/Thy/thy_resources.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
PIDE resources for theory files. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Thy_Resources |
|
11 |
{ |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
12 |
/* PIDE session */ |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
13 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
14 |
def start_session( |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
15 |
options: Options, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
16 |
session_name: String, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
17 |
session_dirs: List[Path] = Nil, |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
18 |
session_base: Option[Sessions.Base] = None, |
67869 | 19 |
print_mode: List[String] = Nil, |
20 |
progress: Progress = No_Progress, |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
21 |
log: Logger = No_Logger): Session = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
22 |
{ |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
23 |
val base = |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
val resources = new Thy_Resources(base, log = log) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
27 |
val session = new Session(options, resources) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
28 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
29 |
val session_error = Future.promise[String] |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
30 |
var session_phase: Session.Consumer[Session.Phase] = null |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
31 |
session_phase = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
32 |
Session.Consumer(getClass.getName) { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
33 |
case Session.Ready => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
34 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
35 |
session_error.fulfill("") |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
36 |
case Session.Terminated(result) if !result.ok => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
37 |
session.phase_changed -= session_phase |
67869 | 38 |
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
|
39 |
case _ => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
40 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
41 |
session.phase_changed += session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
42 |
|
67877 | 43 |
progress.echo("Starting " + session_name + " ...") |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
44 |
Isabelle_Process.start(session, options, |
67869 | 45 |
logic = session_name, dirs = session_dirs, modes = print_mode) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
46 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
47 |
session_error.join match { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
48 |
case "" => session |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
49 |
case msg => session.stop(); error(msg) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
50 |
} |
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 |
|
67879 | 53 |
sealed case class Theories_Result( |
67883 | 54 |
val nodes: List[(Document.Node.Name, Protocol.Node_Status)], |
55 |
val state: Document.State, |
|
56 |
val version: Document.Version) |
|
67879 | 57 |
{ |
67883 | 58 |
def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) |
67879 | 59 |
} |
60 |
||
67063 | 61 |
class Session private[Thy_Resources]( |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
62 |
session_options: Options, |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
63 |
override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) |
67063 | 64 |
{ |
65 |
session => |
|
66 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
67 |
def use_theories( |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
68 |
theories: List[(String, Position.T)], |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
69 |
qualifier: String = Sessions.DRAFT, |
67881 | 70 |
master_dir: String = "", |
67885 | 71 |
id: UUID = UUID(), |
67881 | 72 |
progress: Progress = No_Progress): Theories_Result = |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
73 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
74 |
val dep_theories = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
75 |
resources.load_theories(session, id, theories, qualifier = qualifier, |
67881 | 76 |
master_dir = master_dir, progress = progress) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
77 |
|
67879 | 78 |
val result = Future.promise[Theories_Result] |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
79 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
80 |
def check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
81 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
82 |
val state = session.current_state() |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
83 |
state.stable_tip_version match { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
84 |
case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) => |
67883 | 85 |
def status(name: Document.Node.Name): Protocol.Node_Status = |
86 |
Protocol.node_status(state, version, name, version.nodes(name)) |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
87 |
val nodes = for (name <- dep_theories) yield (name -> status(name)) |
67883 | 88 |
try { result.fulfill(Theories_Result(nodes, state, version)) } |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
89 |
catch { case _: IllegalStateException => } |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
90 |
case _ => |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
91 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
92 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
93 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
94 |
val consumer = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
95 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
96 |
case changed => if (dep_theories.exists(changed.nodes)) check_state |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
97 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
98 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
99 |
session.commands_changed += consumer |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
100 |
check_state |
67879 | 101 |
result.join |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
102 |
session.commands_changed -= consumer |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
103 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
104 |
resources.unload_theories(session, id, dep_theories) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
105 |
|
67879 | 106 |
result.join |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
107 |
} |
67063 | 108 |
} |
109 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
110 |
|
67054 | 111 |
/* internal state */ |
112 |
||
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
113 |
sealed case class State( |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
114 |
required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
115 |
theories: Map[Document.Node.Name, Theory] = Map.empty) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
116 |
{ |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
117 |
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
118 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
119 |
def insert_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
120 |
copy(required = (required /: names)(_.insert(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
121 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
122 |
def remove_required(id: UUID, names: List[Document.Node.Name]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
123 |
copy(required = (required /: names)(_.remove(_, id))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
124 |
|
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
125 |
def update_theories(update: List[(Document.Node.Name, Theory)]): State = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
126 |
copy(theories = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
127 |
(theories /: update)({ case (thys, (name, thy)) => |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
128 |
thys.get(name) match { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
129 |
case Some(thy1) if thy1 == thy => thys |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
130 |
case _ => thys + (name -> thy) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
131 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
132 |
})) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
133 |
} |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
134 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
135 |
final class Theory private[Thy_Resources]( |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
136 |
val node_name: Document.Node.Name, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
137 |
val node_header: Document.Node.Header, |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
138 |
val text: String, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
139 |
val node_required: Boolean) |
67056 | 140 |
{ |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
141 |
override def toString: String = node_name.toString |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
142 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
143 |
def node_perspective: Document.Node.Perspective_Text = |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
144 |
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
|
145 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
146 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
147 |
{ |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
148 |
val (text_edits, old_required) = |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
149 |
if (old.isEmpty) (Text.Edit.inserts(0, text), false) |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
150 |
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
|
151 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
152 |
if (text_edits.isEmpty && node_required == old_required) Nil |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
153 |
else |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
154 |
List(node_name -> Document.Node.Deps(node_header), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
155 |
node_name -> Document.Node.Edits(text_edits), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
156 |
node_name -> node_perspective) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
157 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
158 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
159 |
def required(required: Boolean): Theory = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
160 |
if (required == node_required) this |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
161 |
else new Theory(node_name, node_header, text, required) |
67056 | 162 |
} |
67054 | 163 |
} |
164 |
||
67056 | 165 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 166 |
extends Resources(session_base, log = log) |
167 |
{ |
|
67056 | 168 |
resources => |
169 |
||
67054 | 170 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 171 |
|
172 |
def load_theories( |
|
173 |
session: Session, |
|
67885 | 174 |
id: UUID, |
67056 | 175 |
theories: List[(String, Position.T)], |
176 |
qualifier: String = Sessions.DRAFT, |
|
67881 | 177 |
master_dir: String = "", |
178 |
progress: Progress = No_Progress): List[Document.Node.Name] = |
|
67056 | 179 |
{ |
180 |
val import_names = |
|
181 |
for ((thy, pos) <- theories) |
|
182 |
yield (import_name(qualifier, master_dir, thy), pos) |
|
183 |
||
67881 | 184 |
val dependencies = resources.dependencies(import_names, progress = progress).check_errors |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
185 |
val dep_theories = dependencies.theories |
67888 | 186 |
|
187 |
val loaded_theories = |
|
188 |
for (node_name <- dep_theories) |
|
189 |
yield { |
|
190 |
val path = node_name.path |
|
191 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
|
192 |
||
193 |
progress.expose_interrupt() |
|
194 |
val text = File.read(path) |
|
195 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
|
196 |
new Thy_Resources.Theory(node_name, node_header, text, true) |
|
197 |
} |
|
67056 | 198 |
|
199 |
val edits = |
|
200 |
state.change_result(st => |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
201 |
{ |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
202 |
val st1 = st.insert_required(id, dep_theories) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
203 |
val theory_edits = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
204 |
for (theory <- loaded_theories) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
205 |
yield { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
206 |
val node_name = theory.node_name |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
207 |
val theory1 = theory.required(st1.is_required(node_name)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
208 |
val edits = theory1.node_edits(st1.theories.get(node_name)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
209 |
(edits, (node_name, theory1)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
210 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
211 |
(theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
212 |
}) |
67056 | 213 |
session.update(Document.Blobs.empty, edits) |
214 |
||
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
215 |
dep_theories |
67056 | 216 |
} |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
217 |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
218 |
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
|
219 |
{ |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
220 |
val edits = |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
221 |
state.change_result(st => |
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
222 |
{ |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
223 |
val st1 = st.remove_required(id, dep_theories) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
224 |
val theory_edits = |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
225 |
for { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
226 |
node_name <- dep_theories |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
227 |
theory <- st1.theories.get(node_name) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
228 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
229 |
yield { |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
230 |
val theory1 = theory.required(st1.is_required(node_name)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
231 |
val edits = theory1.node_edits(Some(theory)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
232 |
(edits, (node_name, theory1)) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
233 |
} |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
234 |
(theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) |
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
235 |
}) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
236 |
session.update(Document.Blobs.empty, edits) |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
237 |
} |
67054 | 238 |
} |