equal
deleted
inserted
replaced
30 (** thread management **) |
30 (** thread management **) |
31 |
31 |
32 val implode_desc = op ^ o apfst quote |
32 val implode_desc = op ^ o apfst quote |
33 |
33 |
34 fun implode_message (workers, work) = |
34 fun implode_message (workers, work) = |
35 space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work |
35 space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work |
36 |
36 |
37 |
37 |
38 (* data structures over threads *) |
38 (* data structures over threads *) |
39 |
39 |
40 structure Thread_Heap = Heap |
40 structure Thread_Heap = Heap |