isabelle: src/Tools/jEdit/src/jedit/output_dockable.scala@ed147003de4b (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	{
38223 2a368e8e0a80 more explicit treatment of Swing thread context; wenzelm parents: 38152 diff changeset	25	Swing_Thread.require()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	26
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37132 diff changeset	27	val html_panel =
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37132 diff changeset	28	new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	29	add(html_panel, BorderLayout.CENTER)
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	30
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	31
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	32	/* component state -- owned by Swing thread */
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	33
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	34	private var zoom_factor = 100
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	35	private var show_debug = false
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	36	private var show_tracing = false
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	37	private var follow_caret = true
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	38	private var current_command: Option[Command] = None
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	39
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	40
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	41	private def handle_resize()
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	42	{
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	43	Swing_Thread.now {
37164 8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37132 diff changeset	44	html_panel.resize(Isabelle.font_family(),
8b4617ad1593 reuse main view.font from jEdit; wenzelm parents: 37132 diff changeset	45	scala.math.round(Isabelle.font_size() * zoom_factor / 100))
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	46	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	47	}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	48
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	49	private def handle_perspective(): Boolean =
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	50	Swing_Thread.now {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	51	Document_View(view.getTextArea) match {
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	52	case Some(doc_view) =>
4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	53	val cmd = doc_view.selected_command()
4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	54	if (current_command == cmd) false
4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	55	else { current_command = cmd; true }
4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	56	case None => false
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	57	}
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	58	}
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	59
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	60	private def handle_update(restriction: Option[Set[Command]] = None)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	61	{
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	62	Swing_Thread.now {
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	63	if (follow_caret) handle_perspective()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	64	Document_View(view.getTextArea) match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	65	case Some(doc_view) =>
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	66	current_command match {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	67	case Some(cmd) if !restriction.isDefined \|\| restriction.get.contains(cmd) =>
38152 eab0d1c2e46e Change.Snapshot: include from_current/to_current here, with precomputed changes; wenzelm parents: 38151 diff changeset	68	val snapshot = doc_view.model.snapshot()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	69	val filtered_results =
38152 eab0d1c2e46e Change.Snapshot: include from_current/to_current here, with precomputed changes; wenzelm parents: 38151 diff changeset	70	snapshot.document.current_state(cmd).results filter {
38230 ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; wenzelm parents: 38223 diff changeset	71	case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple; wenzelm parents: 38223 diff changeset	72	case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	73	case _ => true
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	html_panel.render(filtered_results)
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	76	case _ =>
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	case None =>
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	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	81	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	82
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	83
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	84	/* main actor */
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	85
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	86	private val main_actor = actor {
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	87	loop {
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	88	react {
37019 8f747cee4e27 zoom font size; wenzelm parents: 37017 diff changeset	89	case Session.Global_Settings => handle_resize()
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	90	case Command_Set(changed) => handle_update(Some(changed))
37850 afb5653a3a47 observe follow_caret (again); wenzelm parents: 37849 diff changeset	91	case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	92	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	93	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	94	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	95	}
34428 d69fd18f37f9 basic setup of anti-aliasing, according to jEdit property; wenzelm parents: 34424 diff changeset	96
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	97	override def init()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	98	{
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	99	Isabelle.session.global_settings += main_actor
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	100	Isabelle.session.commands_changed += main_actor
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	101	Isabelle.session.perspective += main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	102	}
d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	103
37067 31093f3687b5 simplified dockables using class Dockable; wenzelm parents: 37048 diff changeset	104	override def exit()
34777 91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info); wenzelm parents: 34775 diff changeset	105	{
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	106	Isabelle.session.global_settings -= main_actor
37129 4c83696b340e Command.toString: include id for debugging; wenzelm parents: 37067 diff changeset	107	Isabelle.session.commands_changed -= main_actor
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	108	Isabelle.session.perspective -= main_actor
34768 d8d321af1478 back to low-level JPanel, required for addNotify/removeNotify; wenzelm parents: 34765 diff changeset	109	}
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	110
fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	111
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	112	/* resize */
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	113
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	114	addComponentListener(new ComponentAdapter {
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	115	val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
37014 1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	116	override def componentResized(e: ComponentEvent) { delay() }
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	117	})
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	118
1af0f718ffdc handle component resize for output / HTML panel; wenzelm parents: 36993 diff changeset	119
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	120	/* controls */
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	121
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	122	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	123	zoom.tooltip = "Zoom factor for basic font size"
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	124
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	125	private val debug = new CheckBox("Debug") {
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	126	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	127	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	128	debug.selected = show_debug
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	129	debug.tooltip =
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	130	"<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	131
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	132	private val tracing = new CheckBox("Tracing") {
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	133	reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	134	}
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	135	tracing.selected = show_tracing
37372 babe498016e8 tuned tooltips; wenzelm parents: 37164 diff changeset	136	tracing.tooltip = "Indicate output of tracing messages"
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	137
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	138	private val auto_update = new CheckBox("Auto update") {
37130 7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	139	reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
7f18edbbf618 more reactive message handling, notably for follow_caret mode; wenzelm parents: 37129 diff changeset	140	}
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	141	auto_update.selected = follow_caret
37372 babe498016e8 tuned tooltips; wenzelm parents: 37164 diff changeset	142	auto_update.tooltip = "Indicate automatic update following cursor movement"
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	143
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	144	private val update = new Button("Update") {
37849 4f9de312cc23 Session: predefined real time parameters; wenzelm parents: 37372 diff changeset	145	reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	146	}
37372 babe498016e8 tuned tooltips; wenzelm parents: 37164 diff changeset	147	update.tooltip = "Update display according to the command at cursor position"
37131 d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	148
d4697a30bd02 clarified auto_update vs. update; wenzelm parents: 37130 diff changeset	149	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	150	add(controls.peer, BorderLayout.NORTH)
d01da9438170 added checkboxes for debug/tracing filter; wenzelm parents: 37037 diff changeset	151
36988 fd641bc85222 basic controls to freeze/update prover results; wenzelm parents: 36817 diff changeset	152	handle_update()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	153	}

author	wenzelm
	Sat, 07 Aug 2010 22:09:52 +0200
changeset 38230	ed147003de4b
parent 38223	2a368e8e0a80
child 38356	443fb83a21e8
permissions	-rw-r--r--