53 case "" => session |
53 case "" => session |
54 case msg => session.stop(); error(msg) |
54 case msg => session.stop(); error(msg) |
55 } |
55 } |
56 } |
56 } |
57 |
57 |
|
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 |
58 class Theories_Result private[Thy_Resources]( |
66 class Theories_Result private[Thy_Resources]( |
59 val state: Document.State, |
67 val state: Document.State, |
60 val version: Document.Version, |
68 val version: Document.Version, |
61 val nodes: List[(Document.Node.Name, Document_Status.Node_Status)]) |
69 val nodes: List[(Document.Node.Name, Document_Status.Node_Status)]) |
62 { |
70 { |
63 def node_names: List[Document.Node.Name] = nodes.map(_._1) |
71 def node_names: List[Document.Node.Name] = nodes.map(_._1) |
64 def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) |
72 def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) |
65 |
73 def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name) |
66 def snapshot(node_name: Document.Node.Name): Document.Snapshot = |
|
67 { |
|
68 val snapshot = state.snapshot(node_name) |
|
69 assert(version.id == snapshot.version.id) |
|
70 snapshot |
|
71 } |
|
72 } |
74 } |
73 |
75 |
74 val default_check_delay: Double = 0.5 |
76 val default_check_delay: Double = 0.5 |
75 val default_nodes_status_delay: Double = -1.0 |
77 val default_nodes_status_delay: Double = -1.0 |
76 |
78 |
97 /* theories */ |
99 /* theories */ |
98 |
100 |
99 private sealed case class Use_Theories_State( |
101 private sealed case class Use_Theories_State( |
100 last_update: Time = Time.now(), |
102 last_update: Time = Time.now(), |
101 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
103 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
102 already_initialized: Set[Document.Node.Name] = Set.empty) |
104 already_initialized: Set[Document.Node.Name] = Set.empty, |
|
105 already_committed: Set[Document.Node.Name] = Set.empty, |
|
106 result: Promise[Theories_Result] = Future.promise[Theories_Result]) |
103 { |
107 { |
104 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
108 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
105 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
109 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
106 |
110 |
107 def watchdog(watchdog_timeout: Time): Boolean = |
111 def watchdog(watchdog_timeout: Time): Boolean = |
108 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
112 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
109 |
113 |
110 def initialized_theories( |
114 def initialized_theories( |
111 state: Document.State, |
115 state: Document.State, |
112 version: Document.Version, |
116 version: Document.Version, |
113 new_theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) = |
117 theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) = |
114 { |
118 { |
115 val initialized = |
119 val initialized = |
116 for { |
120 for { |
117 name <- new_theories |
121 name <- theories |
118 if !already_initialized(name) && |
122 if !already_initialized(name) && |
119 Document_Status.Node_Status.make(state, version, name).initialized |
123 Document_Status.Node_Status.make(state, version, name).initialized |
120 } yield name |
124 } yield name |
121 (initialized, copy(already_initialized = already_initialized ++ initialized)) |
125 (initialized, copy(already_initialized = already_initialized ++ initialized)) |
|
126 } |
|
127 |
|
128 def cancel_result { result.cancel } |
|
129 def await_result { result.join_result } |
|
130 def join_result: Theories_Result = result.join |
|
131 def check_result( |
|
132 state: Document.State, |
|
133 version: Document.Version, |
|
134 theories: List[Document.Node.Name], |
|
135 beyond_limit: Boolean, |
|
136 watchdog_timeout: Time, |
|
137 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit]) |
|
138 : Use_Theories_State = |
|
139 { |
|
140 val st1 = |
|
141 if (commit.isDefined) { |
|
142 val committed = |
|
143 for { |
|
144 name <- theories |
|
145 if !already_committed(name) && state.node_consolidated(version, name) |
|
146 } |
|
147 yield { |
|
148 val snapshot = stable_snapshot(state, version, name) |
|
149 val status = Document_Status.Node_Status.make(state, version, name) |
|
150 commit.get.apply(snapshot, status) |
|
151 name |
|
152 } |
|
153 copy(already_committed = already_committed ++ committed) |
|
154 } |
|
155 else this |
|
156 |
|
157 if (beyond_limit || watchdog(watchdog_timeout) || |
|
158 theories.forall(name => |
|
159 already_committed(name) || |
|
160 state.node_consolidated(version, name) || |
|
161 nodes_status.quasi_consolidated(name))) |
|
162 { |
|
163 val nodes = |
|
164 for (name <- theories) |
|
165 yield { (name -> Document_Status.Node_Status.make(state, version, name)) } |
|
166 try { result.fulfill(new Theories_Result(state, version, nodes)) } |
|
167 catch { case _: IllegalStateException => } |
|
168 } |
|
169 |
|
170 st1 |
122 } |
171 } |
123 } |
172 } |
124 |
173 |
125 def use_theories( |
174 def use_theories( |
126 theories: List[String], |
175 theories: List[String], |
129 check_delay: Time = Time.seconds(default_check_delay), |
178 check_delay: Time = Time.seconds(default_check_delay), |
130 check_limit: Int = 0, |
179 check_limit: Int = 0, |
131 watchdog_timeout: Time = Time.zero, |
180 watchdog_timeout: Time = Time.zero, |
132 nodes_status_delay: Time = Time.seconds(default_nodes_status_delay), |
181 nodes_status_delay: Time = Time.seconds(default_nodes_status_delay), |
133 id: UUID = UUID(), |
182 id: UUID = UUID(), |
|
183 // commit: must not block, must not fail |
|
184 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, |
134 progress: Progress = No_Progress): Theories_Result = |
185 progress: Progress = No_Progress): Theories_Result = |
135 { |
186 { |
136 val dep_theories = |
187 val dep_theories = |
137 { |
188 { |
138 val master = proper_string(master_dir) getOrElse tmp_dir_name |
189 val master = proper_string(master_dir) getOrElse tmp_dir_name |
141 resources.dependencies(import_names, progress = progress).check_errors.theories |
192 resources.dependencies(import_names, progress = progress).check_errors.theories |
142 } |
193 } |
143 val dep_theories_set = dep_theories.toSet |
194 val dep_theories_set = dep_theories.toSet |
144 |
195 |
145 val use_theories_state = Synchronized(Use_Theories_State()) |
196 val use_theories_state = Synchronized(Use_Theories_State()) |
146 val result = Future.promise[Theories_Result] |
197 |
147 |
198 def check_result(beyond_limit: Boolean = false) |
148 def check_state(beyond_limit: Boolean = false) |
|
149 { |
199 { |
150 val state = session.current_state() |
200 val state = session.current_state() |
151 state.stable_tip_version match { |
201 state.stable_tip_version match { |
152 case Some(version) => |
202 case Some(version) => |
153 val st = use_theories_state.value |
203 use_theories_state.change( |
154 if (beyond_limit || st.watchdog(watchdog_timeout) || |
204 _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit)) |
155 dep_theories.forall(name => |
|
156 state.node_consolidated(version, name) || |
|
157 st.nodes_status.quasi_consolidated(name))) |
|
158 { |
|
159 val nodes = |
|
160 for (name <- dep_theories) |
|
161 yield (name -> Document_Status.Node_Status.make(state, version, name)) |
|
162 try { result.fulfill(new Theories_Result(state, version, nodes)) } |
|
163 catch { case _: IllegalStateException => } |
|
164 } |
|
165 case None => |
205 case None => |
166 } |
206 } |
167 } |
207 } |
168 |
208 |
169 val check_progress = |
209 val check_progress = |
170 { |
210 { |
171 var check_count = 0 |
211 var check_count = 0 |
172 Event_Timer.request(Time.now(), repeat = Some(check_delay)) |
212 Event_Timer.request(Time.now(), repeat = Some(check_delay)) |
173 { |
213 { |
174 if (progress.stopped) result.cancel |
214 if (progress.stopped) use_theories_state.value.cancel_result |
175 else { |
215 else { |
176 check_count += 1 |
216 check_count += 1 |
177 check_state(check_limit > 0 && check_count > check_limit) |
217 check_result(check_limit > 0 && check_count > check_limit) |
178 } |
218 } |
179 } |
219 } |
180 } |
220 } |
181 |
221 |
182 val consumer = |
222 val consumer = |
233 } |
273 } |
234 |
274 |
235 for ((theory, percentage) <- theory_percentages) |
275 for ((theory, percentage) <- theory_percentages) |
236 progress.theory_percentage("", theory, percentage) |
276 progress.theory_percentage("", theory, percentage) |
237 |
277 |
238 check_state() |
278 check_result() |
239 } |
279 } |
240 } |
280 } |
241 } |
281 } |
242 |
282 |
243 try { |
283 try { |
244 session.commands_changed += consumer |
284 session.commands_changed += consumer |
245 resources.load_theories(session, id, dep_theories, progress) |
285 resources.load_theories(session, id, dep_theories, progress) |
246 result.join_result |
286 use_theories_state.value.await_result |
247 check_progress.cancel |
287 check_progress.cancel |
248 } |
288 } |
249 finally { |
289 finally { |
250 session.commands_changed -= consumer |
290 session.commands_changed -= consumer |
251 resources.unload_theories(session, id, dep_theories) |
291 resources.unload_theories(session, id, dep_theories) |
252 } |
292 } |
253 |
293 |
254 result.join |
294 use_theories_state.value.join_result |
255 } |
295 } |
256 |
296 |
257 def purge_theories( |
297 def purge_theories( |
258 theories: List[String], |
298 theories: List[String], |
259 qualifier: String = Sessions.DRAFT, |
299 qualifier: String = Sessions.DRAFT, |