isabelle: src/Tools/jEdit/src/jedit/output_dockable.scala@7f18edbbf618 (annotated)

36760 b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	1	/* Title: Tools/jEdit/src/jedit/output_dockable.scala
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	2	Author: Makarius
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	3
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	4	Dockable window with result message output.
b82a698ef6c9 tuned headers; wenzelm parents: 36015 diff changeset	5	*/
34408 ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	6
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	7	package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	8
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	9
36015 6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	10	import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 34871 diff changeset	11
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	12	import scala.actors.Actor._
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	13
37017 cf6625012282 try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel); wenzelm parents: 37014 diff changeset	14	import scala.swing.{FlowPanel, Button, CheckBox}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	15	import scala.swing.event.ButtonClicked
fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	16
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	17	import java.awt.BorderLayout
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	18	import java.awt.event.{ComponentEvent, ComponentAdapter}
34748 a2ed621f5f52 reduced logging; wenzelm parents: 34747 diff changeset	19
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	20	import org.gjt.sp.jedit.View
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	21
34765 63ba7f0931e2 generic HTML_Panel -- specific Results_Dockable; wenzelm parents: 34760 diff changeset	22
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	23	class Output_Dockable(view: View, position: String) extends Dockable(view, position)
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	24	{
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	25	Swing_Thread.assert()
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	26
37036 49559c4e85f9 HTML_Panel.handler as overridable method; wenzelm parents: 37033 diff changeset	27	val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	28	add(html_panel, BorderLayout.CENTER)
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	29
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	30
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	31	/* component state -- owned by Swing thread */
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	32
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	33	private var zoom_factor = 100
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	34
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	35	private def handle_resize() =
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	36	Swing_Thread.now {
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	37	html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	38	}
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	39
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	40
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	41	private var current_command: Option[Command] = None
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	42	private var follow_caret = true
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	43	private var show_debug = false
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	44	private var show_tracing = false
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	45
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	46	private def handle_update(restriction: Option[Set[Command]] = None)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	47	{
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	48	Swing_Thread.now {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	49	Document_View(view.getTextArea) match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	50	case Some(doc_view) =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	51	if (follow_caret) current_command = doc_view.selected_command
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	52	current_command match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	53	case Some(cmd) if !restriction.isDefined \|\| restriction.get.contains(cmd) =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	54	val document = doc_view.model.recent_document
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	55	val filtered_results =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	56	document.current_state(cmd).results filter {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	57	case XML.Elem(Markup.TRACING, _, _) => show_tracing
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	58	case XML.Elem(Markup.DEBUG, _, _) => show_debug
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	59	case _ => true
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	60	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	61	html_panel.render(filtered_results)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	62	case _ =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	63	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	64	case None =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	65	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	66	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	67	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	68
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	69
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	70	/* main actor */
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	71
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	72	private val main_actor = actor {
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	73	loop {
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	74	react {
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	75	case Session.Global_Settings => handle_resize()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	76	case Command_Set(changed) => handle_update(Some(changed))
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	77	case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	78	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	79	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	80	}
34428 d69fd18f37f9 basic setup of anti-aliasing, according to jEdit property; wenzelm parents: 34424 diff changeset	81
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	82	override def init()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	83	{
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	84	Isabelle.session.commands_changed += main_actor
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	85	Isabelle.session.global_settings += main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	86	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	87
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	88	override def exit()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	89	{
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	90	Isabelle.session.commands_changed -= main_actor
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	91	Isabelle.session.global_settings -= main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	92	}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	93
fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	94
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	95	/* resize */
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	96
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	97	addComponentListener(new ComponentAdapter {
37033 0e4073f19825 component resize: full handle_resize; wenzelm parents: 37019 diff changeset	98	val delay = Swing_Thread.delay_last(500) { handle_resize() }
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	99	override def componentResized(e: ComponentEvent) { delay() }
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	100	})
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	101
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	102
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	103	/* controls */
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	104
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	105	private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	106	zoom.tooltip = "Zoom factor for basic font size"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	107
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	108	private val update = new Button("Update") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	109	reactions += { case ButtonClicked(_) => handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	110	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	111	update.tooltip =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	112	"<html>Update display according to the<br>state of command at caret position</html>"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	113
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	114	private val tracing = new CheckBox("Tracing") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	115	reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	116	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	117	tracing.selected = show_tracing
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	118	tracing.tooltip =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	119	"<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	120
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	121	private val debug = new CheckBox("Debug") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	122	reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	123	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	124	debug.selected = show_debug
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	125	debug.tooltip =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	126	"<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	127
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	128	private val follow = new CheckBox("Follow") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	129	reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	130	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	131	follow.selected = follow_caret
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	132	follow.tooltip = "<html>Indicate automatic update following cursor movement</html>"
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	133
37039 d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	134	val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	135	add(controls.peer, BorderLayout.NORTH)
d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	136
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	137	handle_update()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	138	}

author	wenzelm
	Thu, 27 May 2010 12:03:59 +0200
changeset 37130	7f18edbbf618
parent 37129	4c83696b340e
child 37131	d4697a30bd02
permissions	-rw-r--r--