42 |
42 |
43 def ok: Boolean = |
43 def ok: Boolean = |
44 (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
44 (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
45 } |
45 } |
46 |
46 |
|
47 private object Checkpoints_State |
|
48 { |
|
49 object Status extends Enumeration |
|
50 { |
|
51 val INIT, LOADED, LOADED_DESCENDANTS = Value |
|
52 } |
|
53 |
|
54 def init(nodes: List[Document.Node.Name]): Checkpoints_State = |
|
55 Checkpoints_State(Status.INIT, nodes) |
|
56 |
|
57 val last: Checkpoints_State = |
|
58 Checkpoints_State(Status.LOADED_DESCENDANTS, Nil) |
|
59 } |
|
60 |
|
61 private sealed case class Checkpoints_State( |
|
62 status: Checkpoints_State.Status.Value, |
|
63 nodes: List[Document.Node.Name]) |
|
64 { |
|
65 def next( |
|
66 dep_graph: Document.Theory_Graph[Unit], |
|
67 finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Checkpoints_State) = |
|
68 { |
|
69 import Checkpoints_State.Status |
|
70 |
|
71 def descendants: List[Document.Node.Name] = |
|
72 nodes match { |
|
73 case Nil => dep_graph.topological_order |
|
74 case current :: rest => |
|
75 val dep_graph1 = |
|
76 if (rest.isEmpty) dep_graph |
|
77 else { |
|
78 val exclude = dep_graph.all_succs(rest).toSet |
|
79 dep_graph.restrict(name => !exclude(name)) |
|
80 } |
|
81 dep_graph1.all_succs(List(current)) |
|
82 } |
|
83 |
|
84 def requirements: List[Document.Node.Name] = |
|
85 dep_graph.all_preds(nodes.headOption.toList).reverse |
|
86 |
|
87 val (load_theories, st1) = |
|
88 (status, nodes) match { |
|
89 case (Status.INIT, Nil) => |
|
90 (descendants, Checkpoints_State.last) |
|
91 case (Status.INIT, current :: _) => |
|
92 (requirements, copy(status = Status.LOADED)) |
|
93 case (Status.LOADED, current :: rest) if finished(current) => |
|
94 (descendants, copy(status = Status.LOADED_DESCENDANTS)) |
|
95 case (Status.LOADED_DESCENDANTS, _ :: rest) if descendants.forall(finished) => |
|
96 Checkpoints_State.init(rest).next(dep_graph, finished) |
|
97 case _ => (Nil, this) |
|
98 } |
|
99 (load_theories.filterNot(finished), st1) |
|
100 } |
|
101 } |
|
102 |
47 class Session private[Headless]( |
103 class Session private[Headless]( |
48 session_name: String, |
104 session_name: String, |
49 _session_options: => Options, |
105 _session_options: => Options, |
50 override val resources: Resources) extends isabelle.Session(_session_options, resources) |
106 override val resources: Resources) extends isabelle.Session(_session_options, resources) |
51 { |
107 { |
52 session => |
108 session => |
53 |
109 |
54 |
110 |
|
111 private def loaded_theory(name: Document.Node.Name): Boolean = |
|
112 resources.session_base.loaded_theory(name.theory) |
|
113 |
|
114 |
55 /* options */ |
115 /* options */ |
56 |
116 |
57 def default_check_delay: Time = session_options.seconds("headless_check_delay") |
117 def default_check_delay: Time = session_options.seconds("headless_check_delay") |
58 def default_check_limit: Int = session_options.int("headless_check_limit") |
118 def default_check_limit: Int = session_options.int("headless_check_limit") |
59 def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") |
119 def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") |
79 |
139 |
80 |
140 |
81 /* theories */ |
141 /* theories */ |
82 |
142 |
83 private sealed case class Use_Theories_State( |
143 private sealed case class Use_Theories_State( |
|
144 dependencies: resources.Dependencies[Unit], |
|
145 checkpoints_state: Checkpoints_State, |
|
146 watchdog_timeout: Time, |
|
147 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], |
84 last_update: Time = Time.now(), |
148 last_update: Time = Time.now(), |
85 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
149 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
86 already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, |
150 already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, |
87 result: Option[Exn.Result[Use_Theories_Result]] = None) |
151 result: Option[Exn.Result[Use_Theories_Result]] = None) |
88 { |
152 { |
|
153 def dep_graph: Document.Theory_Graph[Unit] = dependencies.theory_graph |
|
154 |
89 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
155 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
90 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
156 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
91 |
157 |
92 def watchdog(watchdog_timeout: Time): Boolean = |
158 def watchdog: Boolean = |
93 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
159 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
94 |
160 |
95 def finished_result: Boolean = result.isDefined |
161 def finished_result: Boolean = result.isDefined |
96 |
162 |
97 def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = |
163 def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = |
98 if (finished_result) Some((result.get, this)) else None |
164 if (finished_result) Some((result.get, this)) else None |
99 |
165 |
100 def cancel_result: Use_Theories_State = |
166 def cancel_result: Use_Theories_State = |
101 if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) |
167 if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) |
102 |
168 |
103 def check_result( |
169 def clean: Set[Document.Node.Name] = |
104 state: Document.State, |
170 already_committed.keySet -- checkpoints_state.nodes |
105 version: Document.Version, |
171 |
106 dep_theories: List[Document.Node.Name], |
172 def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) |
107 beyond_limit: Boolean, |
173 : (List[Document.Node.Name], Use_Theories_State) = |
108 watchdog_timeout: Time, |
|
109 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit]) |
|
110 : Use_Theories_State = |
|
111 { |
174 { |
112 val already_committed1 = |
175 val already_committed1 = |
113 if (commit.isDefined) { |
176 commit match { |
114 (already_committed /: dep_theories)({ case (committed, name) => |
177 case None => already_committed |
115 def parents_committed: Boolean = |
178 case Some(commit_fn) => |
116 version.nodes(name).header.imports.forall(parent => |
179 (already_committed /: dep_graph.topological_order)( |
117 resources.session_base.loaded_theory(parent) || committed.isDefinedAt(parent)) |
180 { case (committed, name) => |
118 if (!committed.isDefinedAt(name) && parents_committed && |
181 def parents_committed: Boolean = |
119 state.node_consolidated(version, name)) |
182 version.nodes(name).header.imports.forall(parent => |
120 { |
183 loaded_theory(parent) || committed.isDefinedAt(parent)) |
121 val snapshot = stable_snapshot(state, version, name) |
184 if (!committed.isDefinedAt(name) && parents_committed && |
122 val status = Document_Status.Node_Status.make(state, version, name) |
185 state.node_consolidated(version, name)) |
123 commit.get.apply(snapshot, status) |
186 { |
124 committed + (name -> status) |
187 val snapshot = stable_snapshot(state, version, name) |
125 } |
188 val status = Document_Status.Node_Status.make(state, version, name) |
126 else committed |
189 commit_fn(snapshot, status) |
127 }) |
190 committed + (name -> status) |
128 } |
191 } |
129 else already_committed |
192 else committed |
|
193 }) |
|
194 } |
130 |
195 |
131 val result1 = |
196 val result1 = |
132 if (!finished_result && |
197 if (!finished_result && |
133 (beyond_limit || watchdog(watchdog_timeout) || |
198 (beyond_limit || watchdog || |
134 dep_theories.forall(name => |
199 dep_graph.keys_iterator.forall(name => |
135 already_committed1.isDefinedAt(name) || |
200 already_committed1.isDefinedAt(name) || |
136 state.node_consolidated(version, name) || |
201 state.node_consolidated(version, name) || |
137 nodes_status.quasi_consolidated(name)))) |
202 nodes_status.quasi_consolidated(name)))) |
138 { |
203 { |
139 val nodes = |
204 val nodes = |
140 for (name <- dep_theories) |
205 (for (name <- dep_graph.keys_iterator) |
141 yield { (name -> Document_Status.Node_Status.make(state, version, name)) } |
206 yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList |
142 val nodes_committed = |
207 val nodes_committed = |
143 for { |
208 (for { |
144 name <- dep_theories |
209 name <- dep_graph.keys_iterator |
145 status <- already_committed1.get(name) |
210 status <- already_committed1.get(name) |
146 } yield (name -> status) |
211 } yield (name -> status)).toList |
147 Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) |
212 Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) |
148 } |
213 } |
149 else result |
214 else result |
150 |
215 |
151 copy(already_committed = already_committed1, result = result1) |
216 val (load_theories, checkpoints_state1) = |
|
217 checkpoints_state.next(dep_graph, |
|
218 name => |
|
219 loaded_theory(name) || |
|
220 already_committed1.isDefinedAt(name) || |
|
221 nodes_status.consolidated(name)) |
|
222 |
|
223 (load_theories, |
|
224 copy(already_committed = already_committed1, result = result1, |
|
225 checkpoints_state = checkpoints_state1)) |
152 } |
226 } |
153 } |
227 } |
154 |
228 |
155 def use_theories( |
229 def use_theories( |
156 theories: List[String], |
230 theories: List[String], |
161 check_limit: Int = default_check_limit, |
235 check_limit: Int = default_check_limit, |
162 watchdog_timeout: Time = default_watchdog_timeout, |
236 watchdog_timeout: Time = default_watchdog_timeout, |
163 nodes_status_delay: Time = default_nodes_status_delay, |
237 nodes_status_delay: Time = default_nodes_status_delay, |
164 id: UUID.T = UUID.random(), |
238 id: UUID.T = UUID.random(), |
165 share_common_data: Boolean = false, |
239 share_common_data: Boolean = false, |
|
240 checkpoints: Set[Document.Node.Name] = Set.empty, |
166 // commit: must not block, must not fail |
241 // commit: must not block, must not fail |
167 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, |
242 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, |
168 commit_cleanup_delay: Time = default_commit_cleanup_delay, |
243 commit_cleanup_delay: Time = default_commit_cleanup_delay, |
169 progress: Progress = No_Progress): Use_Theories_Result = |
244 progress: Progress = No_Progress): Use_Theories_Result = |
170 { |
245 { |
174 theories.map(thy => |
249 theories.map(thy => |
175 resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) |
250 resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) |
176 resources.dependencies(import_names, progress = progress).check_errors |
251 resources.dependencies(import_names, progress = progress).check_errors |
177 } |
252 } |
178 val dep_theories = dependencies.theories |
253 val dep_theories = dependencies.theories |
|
254 val dep_theories_set = dep_theories.toSet |
179 val dep_files = |
255 val dep_files = |
180 dependencies.loaded_files(false).flatMap(_._2). |
256 dependencies.loaded_files(false).flatMap(_._2). |
181 map(path => Document.Node.Name(resources.append("", path))) |
257 map(path => Document.Node.Name(resources.append("", path))) |
182 |
258 |
183 val use_theories_state = Synchronized(Use_Theories_State()) |
259 val use_theories_state = |
184 |
260 { |
185 def check_result_state(beyond_limit: Boolean = false) |
261 val checkpoints_state = |
|
262 Checkpoints_State.init( |
|
263 if (checkpoints.isEmpty) Nil |
|
264 else dependencies.theory_graph.topological_order.filter(checkpoints(_))) |
|
265 Synchronized(Use_Theories_State(dependencies, checkpoints_state, watchdog_timeout, commit)) |
|
266 } |
|
267 |
|
268 def check_state(beyond_limit: Boolean = false) |
186 { |
269 { |
187 val state = session.current_state() |
270 val state = session.current_state() |
188 state.stable_tip_version match { |
271 for (version <- state.stable_tip_version) { |
189 case Some(version) => |
272 val load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit)) |
190 use_theories_state.change( |
273 if (load_theories.nonEmpty) { |
191 _.check_result(state, version, dep_theories, beyond_limit, watchdog_timeout, commit)) |
274 resources.load_theories( |
192 case None => |
275 session, id, load_theories, dep_files, unicode_symbols, share_common_data, progress) |
|
276 } |
193 } |
277 } |
194 } |
278 } |
195 |
279 |
196 val check_progress = |
280 val check_progress = |
197 { |
281 { |