isabelle: src/Tools/jEdit/src/jedit/output_dockable.scala@d4697a30bd02 (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
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	34	private var show_debug = false
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	35	private var show_tracing = false
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	36	private var follow_caret = true
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	37	private var current_command: Option[Command] = None
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	38
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	39
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	40	private def handle_resize()
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	41	{
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	42	Swing_Thread.now {
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	43	html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	44	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	45	}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	46
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	47	private def handle_caret()
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	48	{
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	49	Swing_Thread.now {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	50	Document_View(view.getTextArea) match {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	51	case Some(doc_view) => current_command = doc_view.selected_command
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	52	case None =>
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	53	}
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	54	}
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	55	}
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	56
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	57	private def handle_update(restriction: Option[Set[Command]] = None)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	58	{
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	59	Swing_Thread.now {
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	60	if (follow_caret) handle_caret()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	61	Document_View(view.getTextArea) match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	62	case Some(doc_view) =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	63	current_command match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	64	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	65	val document = doc_view.model.recent_document
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	66	val filtered_results =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	67	document.current_state(cmd).results filter {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	68	case XML.Elem(Markup.TRACING, _, _) => show_tracing
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	69	case XML.Elem(Markup.DEBUG, _, _) => show_debug
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	70	case _ => true
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	71	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	72	html_panel.render(filtered_results)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	73	case _ =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	74	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	75	case None =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	76	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	77	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	78	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	79
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	80
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	81	/* main actor */
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	82
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	83	private val main_actor = actor {
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	84	loop {
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	85	react {
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	86	case Session.Global_Settings => handle_resize()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	87	case Command_Set(changed) => handle_update(Some(changed))
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	88	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	89	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	90	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	91	}
34428 d69fd18f37f9 basic setup of anti-aliasing, according to jEdit property; wenzelm parents: 34424 diff changeset	92
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	93	override def init()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	94	{
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	95	Isabelle.session.commands_changed += main_actor
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	96	Isabelle.session.global_settings += main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	97	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	98
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	99	override def exit()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	100	{
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	101	Isabelle.session.commands_changed -= main_actor
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	102	Isabelle.session.global_settings -= main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	103	}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	104
fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	105
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	106	/* resize */
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	107
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	108	addComponentListener(new ComponentAdapter {
37033 0e4073f19825 component resize: full handle_resize; wenzelm parents: 37019 diff changeset	109	val delay = Swing_Thread.delay_last(500) { handle_resize() }
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	110	override def componentResized(e: ComponentEvent) { delay() }
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	111	})
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	112
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	113
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	114	/* controls */
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	115
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	116	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	117	zoom.tooltip = "Zoom factor for basic font size"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	118
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	119	private val debug = new CheckBox("Debug") {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	120	reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	121	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	122	debug.selected = show_debug
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	123	debug.tooltip =
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	124	"<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	125
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	126	private val tracing = new CheckBox("Tracing") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	127	reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	128	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	129	tracing.selected = show_tracing
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	130	tracing.tooltip =
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	131	"<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	132
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	133	private val auto_update = new CheckBox("Auto update") {
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	134	reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	135	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	136	auto_update.selected = follow_caret
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	137	auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	138
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	139	private val update = new Button("Update") {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	140	reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	141	}
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	142	update.tooltip = "<html>Update display according to the command at cursor position</html>"
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	143
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	144	val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
37039 d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	145	add(controls.peer, BorderLayout.NORTH)
d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	146
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	147	handle_update()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	148	}

author	wenzelm
	Thu, 27 May 2010 12:34:30 +0200
changeset 37131	d4697a30bd02
parent 37130	7f18edbbf618
child 37132	10ef4da1c314
permissions	-rw-r--r--