equal
deleted
inserted
replaced
25 if (do_update && !snapshot.is_outdated) { |
25 if (do_update && !snapshot.is_outdated) { |
26 snapshot.current_command(caret.node_name, caret.offset) match { |
26 snapshot.current_command(caret.node_name, caret.offset) match { |
27 case None => copy(output = Nil) |
27 case None => copy(output = Nil) |
28 case Some(command) => |
28 case Some(command) => |
29 copy(output = |
29 copy(output = |
30 if (restriction.isEmpty || restriction.get.contains(command)) |
30 if (restriction.isEmpty || restriction.get.contains(command)) { |
31 Rendering.output_messages(snapshot.command_results(command)) |
31 val output_state = resources.options.bool("editor_output_state") |
32 else output) |
32 Rendering.output_messages(snapshot.command_results(command), output_state) |
|
33 } else output) |
33 } |
34 } |
34 } |
35 } |
35 else this |
36 else this |
36 } |
37 } |
37 if (st1.output != output) { |
38 if (st1.output != output) { |