equal
deleted
inserted
replaced
63 else (current_snapshot, current_command, current_results) |
63 else (current_snapshot, current_command, current_results) |
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 = JEdit_Rendering(new_snapshot, PIDE.options.value) |
69 Rendering.output_messages(new_results) |
70 rendering.output_messages(new_results) |
|
71 } |
|
72 else current_output |
70 else current_output |
73 |
71 |
74 if (new_output != current_output) |
72 if (new_output != current_output) |
75 pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output)) |
73 pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output)) |
76 |
74 |