139 |
139 |
140 |
140 |
141 /* theories */ |
141 /* theories */ |
142 |
142 |
143 private sealed case class Use_Theories_State( |
143 private sealed case class Use_Theories_State( |
144 dependencies: resources.Dependencies[Unit], |
144 dep_graph: Document.Node.Name.Graph[Unit], |
145 checkpoints_state: Checkpoints_State, |
145 checkpoints_state: Checkpoints_State, |
146 watchdog_timeout: Time, |
146 watchdog_timeout: Time, |
147 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], |
147 commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], |
148 last_update: Time = Time.now(), |
148 last_update: Time = Time.now(), |
149 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
149 nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
150 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, |
151 result: Option[Exn.Result[Use_Theories_Result]] = None) |
151 result: Option[Exn.Result[Use_Theories_Result]] = None) |
152 { |
152 { |
153 def dep_graph: Document.Node.Name.Graph[Unit] = dependencies.theory_graph |
|
154 |
|
155 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
153 def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
156 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
154 copy(last_update = Time.now(), nodes_status = new_nodes_status) |
157 |
155 |
158 def watchdog: Boolean = |
156 def watchdog: Boolean = |
159 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
157 watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
261 { |
259 { |
262 val checkpoints_state = |
260 val checkpoints_state = |
263 Checkpoints_State.init( |
261 Checkpoints_State.init( |
264 if (checkpoints.isEmpty) Nil |
262 if (checkpoints.isEmpty) Nil |
265 else dependencies.theory_graph.topological_order.filter(checkpoints(_))) |
263 else dependencies.theory_graph.topological_order.filter(checkpoints(_))) |
266 Synchronized(Use_Theories_State(dependencies, checkpoints_state, watchdog_timeout, commit)) |
264 Synchronized( |
|
265 Use_Theories_State(dependencies.theory_graph, checkpoints_state, watchdog_timeout, commit)) |
267 } |
266 } |
268 |
267 |
269 def check_state(beyond_limit: Boolean = false) |
268 def check_state(beyond_limit: Boolean = false) |
270 { |
269 { |
271 val state = session.current_state() |
270 val state = session.current_state() |