equal
deleted
inserted
replaced
56 case _ => |
56 case _ => |
57 if (props.exists(_ == Markup.PADDING_LINE)) |
57 if (props.exists(_ == Markup.PADDING_LINE)) |
58 Isabelle.insert_line_padding(text_area, text) |
58 Isabelle.insert_line_padding(text_area, text) |
59 else text_area.setSelectedText(text) |
59 else text_area.setSelectedText(text) |
60 } |
60 } |
|
61 text_area.requestFocus |
61 |
62 |
62 case Simplifier_Trace.Active(serial, answer) => |
63 case Simplifier_Trace.Active(serial, answer) => |
63 Simplifier_Trace.send_reply(PIDE.session, serial, answer) |
64 Simplifier_Trace.send_reply(PIDE.session, serial, answer) |
64 |
65 |
65 case Protocol.Dialog(id, serial, result) => |
66 case Protocol.Dialog(id, serial, result) => |