| changeset 77731 | 48fbecc8fab1 |
| parent 77723 | b761c91c2447 |
| child 78648 | 852ec09aef13 |
| 77730:4a174bea55e2 | 77731:48fbecc8fab1 |
|---|---|
180 end; |
180 end; |
181 |
181 |
182 end; |
182 end; |
183 |
183 |
184 structure Tasks = Set(type key = task val ord = task_ord); |
184 structure Tasks = Set(type key = task val ord = task_ord); |
185 structure Task_Graph = Graph(type key = task val ord = task_ord); |
185 structure Task_Graph = Graph(Tasks.Key); |
186 |
186 |
187 |
187 |
188 (* timing *) |
188 (* timing *) |
189 |
189 |
190 fun running task = |
190 fun running task = |