isabelle: src/Tools/jEdit/src/raw_output_dockable.scala@0ffcad1f6130 (annotated)

43282 5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory; wenzelm parents: 39588 diff changeset	1	/* Title: Tools/jEdit/src/raw_output_dockable.scala
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	2	Author: Makarius
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	3
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	4	Dockable window for raw process output (stdout).
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	5	*/
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	6
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	7	package isabelle.jedit
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	8
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	9
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	10	import isabelle._
66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: 57612 diff changeset	11	import isabelle.jedit_base.Dockable
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	12
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37065 diff changeset	13	import scala.swing.{TextArea, ScrollPane}
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	14
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	15	import org.gjt.sp.jedit.View
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	16
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	17
49559 c3a6e110679b tuned; wenzelm parents: 49416 diff changeset	18	class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	19	{
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37065 diff changeset	20	private val text_area = new TextArea
31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37065 diff changeset	21	set_content(new ScrollPane(text_area))
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	22
2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	23
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	24	/* main */
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	25
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	26	private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	27	Session.Consumer[Prover.Output](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	28	case output: Prover.Output =>
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 56715 diff changeset	29	GUI_Thread.later {
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	30	text_area.append(XML.content(output.message))
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	31	if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	32	}
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56385 diff changeset	33	}
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	34
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 66591 diff changeset	35	override def init(): Unit = { PIDE.session.raw_output_messages += main }
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 66591 diff changeset	36	override def exit(): Unit = { PIDE.session.raw_output_messages -= main }
37065 2a73253b5898 separate event bus and dockable for raw output (stdout); wenzelm parents: diff changeset	37	}

author	wenzelm
	Mon, 01 Mar 2021 22:22:12 +0100
changeset 73340	0ffcad1f6130
parent 66591	6efa351190d0
child 73987	fc363a3b690a
permissions	-rw-r--r--