equal
deleted
inserted
replaced
64 case None => (current_snapshot, current_command, current_results) |
64 case None => (current_snapshot, current_command, current_results) |
65 } |
65 } |
66 |
66 |
67 val new_output = |
67 val new_output = |
68 if (!restriction.isDefined || restriction.get.contains(new_command)) { |
68 if (!restriction.isDefined || restriction.get.contains(new_command)) { |
69 val rendering = Rendering(new_snapshot, PIDE.options.value) |
69 val rendering = JEdit_Rendering(new_snapshot, PIDE.options.value) |
70 rendering.output_messages(new_results) |
70 rendering.output_messages(new_results) |
71 } |
71 } |
72 else current_output |
72 else current_output |
73 |
73 |
74 if (new_output != current_output) |
74 if (new_output != current_output) |