--- a/src/Tools/jEdit/src/protocol_dockable.scala Wed Aug 12 11:07:14 2020 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Aug 12 11:22:11 2020 +0200
@@ -19,13 +19,6 @@
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
{
- /* controls */
-
- private val ml_stats = new Isabelle.ML_Stats
-
- private val controls = Wrap_Panel(List(ml_stats))
-
-
/* text area */
private val text_area = new TextArea
@@ -34,32 +27,26 @@
/* layout */
set_content(new ScrollPane(text_area))
- add(controls.peer, BorderLayout.NORTH)
/* main */
private val main =
- Session.Consumer[Any](getClass.getName) {
+ Session.Consumer[Prover.Message](getClass.getName) {
case input: Prover.Input =>
GUI_Thread.later { text_area.append(input.toString + "\n\n") }
case output: Prover.Output =>
GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
-
- case _: Session.Global_Options =>
- GUI_Thread.later { ml_stats.load() }
}
override def init()
{
PIDE.session.all_messages += main
- PIDE.session.global_options += main
}
override def exit()
{
PIDE.session.all_messages -= main
- PIDE.session.global_options -= main
}
}