src/Tools/jEdit/src/active.scala
changeset 57593 2f7d91242b99
parent 56999 d926fc73b554
child 57594 037f3b251df5
equal deleted inserted replaced
57592:b73d74d0e428 57593:2f7d91242b99
    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                 text_area.requestFocus
    62 
    62 
    63               case Simplifier_Trace.Active(serial, answer) =>
       
    64                 Simplifier_Trace.send_reply(PIDE.session, serial, answer)
       
    65 
       
    66               case Protocol.Dialog(id, serial, result) =>
    63               case Protocol.Dialog(id, serial, result) =>
    67                 model.session.dialog_result(id, serial, result)
    64                 model.session.dialog_result(id, serial, result)
    68 
    65 
    69               case _ =>
    66               case _ =>
    70             }
    67             }