equal
deleted
inserted
replaced
23 |
23 |
24 object Document_View |
24 object Document_View |
25 { |
25 { |
26 def choose_color(command: Command, doc: Document): Color = |
26 def choose_color(command: Command, doc: Document): Color = |
27 { |
27 { |
28 doc.current_state(command).status match { |
28 val state = doc.current_state(command) |
29 case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
29 if (state.forks > 0) new Color(255, 228, 225) |
30 case Command.Status.FINISHED => new Color(234, 248, 255) |
30 else if (state.forks < 0) Color.red |
31 case Command.Status.FAILED => new Color(255, 193, 193) |
31 else |
32 case Command.Status.UNDEFINED => Color.red |
32 state.status match { |
33 } |
33 case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
|
34 case Command.Status.FINISHED => new Color(234, 248, 255) |
|
35 case Command.Status.FAILED => new Color(255, 193, 193) |
|
36 case Command.Status.UNDEFINED => Color.red |
|
37 } |
34 } |
38 } |
35 |
39 |
36 |
40 |
37 /* document view of text area */ |
41 /* document view of text area */ |
38 |
42 |