equal
deleted
inserted
replaced
37 |
37 |
38 object Command_Timings { |
38 object Command_Timings { |
39 type Entry = (Symbol.Offset, Time) |
39 type Entry = (Symbol.Offset, Time) |
40 val empty: Command_Timings = |
40 val empty: Command_Timings = |
41 new Command_Timings(SortedMap.empty, Time.zero) |
41 new Command_Timings(SortedMap.empty, Time.zero) |
42 def make(args: IterableOnce[Entry]): Command_Timings = |
|
43 args.iterator.foldLeft(empty)(_ + _) |
|
44 def merge(args: IterableOnce[Command_Timings]): Command_Timings = |
42 def merge(args: IterableOnce[Command_Timings]): Command_Timings = |
45 args.iterator.foldLeft(empty)(_ ++ _) |
43 args.iterator.foldLeft(empty)(_ ++ _) |
46 } |
44 } |
47 |
45 |
48 final class Command_Timings private( |
46 final class Command_Timings private( |