isabelle: src/Tools/jEdit/src/query_dockable.scala@8f485a199874 (annotated)

56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	1	/* Title: Tools/jEdit/src/query_dockable.scala
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	2	Author: Makarius
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	3
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	4	Dockable window for query operations.
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	5	*/
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	6
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	7	package isabelle.jedit
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	8
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	9
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	10	import isabelle._
66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: 66206 diff changeset	11	import isabelle.jedit_base.Dockable
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	12
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	13	import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	14	import javax.swing.{JComponent, JTextField}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	15
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	16	import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	17	ComboBox, TabbedPane, BorderPanel}
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	18	import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	19
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	20	import org.gjt.sp.jedit.View
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	21
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	22
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	23	object Query_Dockable
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	24	{
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	25	private abstract class Operation(view: View)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	26	{
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	27	val pretty_text_area = new Pretty_Text_Area(view)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	28	def query_operation: Query_Operation[View]
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	29	def query: JComponent
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	30	def select: Unit
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	31	def page: TabbedPane.Page
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	32	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	33	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	34
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	35	class Query_Dockable(view: View, position: String) extends Dockable(view, position)
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	36	{
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	37	/* common GUI components */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	38
57044 042d6e58cb40 more uniform Font_Info.Zoom_Box; wenzelm parents: 57042 diff changeset	39	private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	40
60861 fa77faa87d5f maintain history more often; wenzelm parents: 60750 diff changeset	41	private def make_query(property: String, tooltip: String, apply_query: () => Unit)
fa77faa87d5f maintain history more often; wenzelm parents: 60750 diff changeset	42	: Completion_Popup.History_Text_Field =
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	43	new Completion_Popup.History_Text_Field(property)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	44	{
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	45	override def processKeyEvent(evt: KeyEvent): Unit =
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	46	{
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	47	if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	48	super.processKeyEvent(evt)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	49	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	50	{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	51	setColumns(40)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	52	setToolTipText(tooltip)
69358 71ef6e6da3dc prefer Isabelle_Fonts.sans (not mono) as derived GUI font; wenzelm parents: 66591 diff changeset	53	setFont(GUI.imitate_font(getFont, scale = 1.2))
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	54	}
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	55
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	56
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	57	/* consume status */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	58
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	59	def consume_status(
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	60	process_indicator: Process_Indicator, status: Query_Operation.Status.Value): Unit =
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	61	{
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	62	status match {
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	63	case Query_Operation.Status.WAITING =>
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	64	process_indicator.update("Waiting for evaluation of context ...", 5)
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	65	case Query_Operation.Status.RUNNING =>
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	66	process_indicator.update("Running find operation ...", 15)
54640 bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command; wenzelm parents: 54368 diff changeset	67	case Query_Operation.Status.FINISHED =>
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	68	process_indicator.update(null, 0)
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	69	}
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	70	}
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	71
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	72
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	73	/* find theorems */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	74
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	75	private val find_theorems = new Query_Dockable.Operation(view)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	76	{
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	77	/* query */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	78
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	79	private val process_indicator = new Process_Indicator
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	80
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	81	val query_operation =
66082 2d12a730a380 clarified modules; wenzelm parents: 65246 diff changeset	82	new Query_Operation(PIDE.editor, view, "find_theorems",
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	83	consume_status(process_indicator, _),
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	84	(snapshot, results, body) =>
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	85	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	86
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	87	private def apply_query(): Unit =
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	88	{
60861 fa77faa87d5f maintain history more often; wenzelm parents: 60750 diff changeset	89	query.addCurrentToHistory()
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	90	query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	91	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	92
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	93	private val query_label = new Label("Find:") {
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	94	tooltip =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	95	GUI.tooltip_lines(
70278 94b332206700 proper message; wenzelm parents: 69358 diff changeset	96	"Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	97	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	98
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	99	val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	100
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	101
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	102	/* GUI page */
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	103
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	104	private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	105	tooltip = "Limit of displayed results"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	106	verifier = (s: String) =>
63805 c272680df665 clarified modules; wenzelm parents: 60861 diff changeset	107	s match { case Value.Int(x) => x >= 0 case _ => false }
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	108	listenTo(keys)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	109	reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	110	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	111
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	112	private val allow_dups = new CheckBox("Duplicates") {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	113	tooltip = "Show all versions of matching theorems"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	114	selected = false
56911 dc3ba749d3b8 tuned GUI; wenzelm parents: 56910 diff changeset	115	reactions += { case ButtonClicked(_) => apply_query() }
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	116	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	117
56910 d1d986a97524 tuned GUI; wenzelm parents: 56909 diff changeset	118	private val apply_button = new Button("<html><b>Apply</b></html>") {
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	119	tooltip = "Find theorems meeting specified criteria"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	120	reactions += { case ButtonClicked(_) => apply_query() }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	121	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	122
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	123	private val control_panel =
66205 e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	124	Wrap_Panel(
e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	125	List(query_label, Component.wrap(query), limit, allow_dups,
e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	126	process_indicator.component, apply_button,
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	127	pretty_text_area.search_label, pretty_text_area.search_field))
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	128
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	129	def select: Unit = { control_panel.contents += zoom }
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	130
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	131	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	132	new TabbedPane.Page("Find Theorems", new BorderPanel {
59391 39a38657d16b tuned; wenzelm parents: 59286 diff changeset	133	layout(control_panel) = BorderPanel.Position.North
39a38657d16b tuned; wenzelm parents: 59286 diff changeset	134	layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	135	}, apply_button.tooltip)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	136	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	137
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	138
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	139	/* find consts */
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	140
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	141	private val find_consts = new Query_Dockable.Operation(view)
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	142	{
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	143	/* query */
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	144
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	145	private val process_indicator = new Process_Indicator
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	146
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	147	val query_operation =
66082 2d12a730a380 clarified modules; wenzelm parents: 65246 diff changeset	148	new Query_Operation(PIDE.editor, view, "find_consts",
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	149	consume_status(process_indicator, _),
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	150	(snapshot, results, body) =>
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	151	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	152
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	153	private def apply_query(): Unit =
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	154	{
60861 fa77faa87d5f maintain history more often; wenzelm parents: 60750 diff changeset	155	query.addCurrentToHistory()
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	156	query_operation.apply_query(List(query.getText))
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	157	}
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	158
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	159	private val query_label = new Label("Find:") {
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	160	tooltip = GUI.tooltip_lines("Name / type patterns for constants")
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	161	}
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	162
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	163	val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	164
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	165
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	166	/* GUI page */
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	167
56910 d1d986a97524 tuned GUI; wenzelm parents: 56909 diff changeset	168	private val apply_button = new Button("<html><b>Apply</b></html>") {
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	169	tooltip = "Find constants by name / type patterns"
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	170	reactions += { case ButtonClicked(_) => apply_query() }
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	171	}
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	172
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	173	private val control_panel =
66205 e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	174	Wrap_Panel(
e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	175	List(
e9fa94f43a15 tuned signature; wenzelm parents: 66082 diff changeset	176	query_label, Component.wrap(query), process_indicator.component, apply_button,
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	177	pretty_text_area.search_label, pretty_text_area.search_field))
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	178
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	179	def select: Unit = { control_panel.contents += zoom }
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	180
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	181	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	182	new TabbedPane.Page("Find Constants", new BorderPanel {
59391 39a38657d16b tuned; wenzelm parents: 59286 diff changeset	183	layout(control_panel) = BorderPanel.Position.North
39a38657d16b tuned; wenzelm parents: 59286 diff changeset	184	layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	185	}, apply_button.tooltip)
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	186	}
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	187
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	188
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	189	/* print operation */
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	190
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	191	private val print_operation = new Query_Dockable.Operation(view)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	192	{
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	193	/* items */
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	194
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	195	private class Item(val name: String, description: String, sel: Boolean)
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	196	{
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	197	val checkbox = new CheckBox(name) {
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	198	tooltip = "Print " + description
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	199	selected = sel
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	200	reactions += { case ButtonClicked(_) => apply_query() }
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	201	}
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	202	}
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	203
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	204	private var _items: List[Item] = Nil
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	205
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	206	private def selected_items(): List[String] =
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	207	for (item <- _items if item.checkbox.selected) yield item.name
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	208
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	209	private def update_items(): List[Item] =
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	210	{
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	211	val old_items = _items
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	212	def was_selected(name: String): Boolean =
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	213	old_items.find(item => item.name == name) match {
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	214	case None => false
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	215	case Some(item) => item.checkbox.selected
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	216	}
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	217
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	218	_items =
72215 8f9cffa78112 clarified signature; wenzelm parents: 71704 diff changeset	219	for ((name, description) <- Print_Operation.get(PIDE.session))
8f9cffa78112 clarified signature; wenzelm parents: 71704 diff changeset	220	yield new Item(name, description, was_selected(name))
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	221	_items
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	222	}
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	223
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	224
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	225	/* query */
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	226
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	227	private val process_indicator = new Process_Indicator
a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	228
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	229	val query_operation =
66082 2d12a730a380 clarified modules; wenzelm parents: 65246 diff changeset	230	new Query_Operation(PIDE.editor, view, "print_operation",
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	231	consume_status(process_indicator, _),
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	232	(snapshot, results, body) =>
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	233	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	234
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	235	private def apply_query(): Unit =
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	236	query_operation.apply_query(selected_items())
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	237
56866 c4512e94e15c tuned GUI; wenzelm parents: 56865 diff changeset	238	private val query_label = new Label("Print:")
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	239	def query: JComponent = apply_button.peer
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	240
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	241	update_items()
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	242
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	243
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	244	/* GUI page */
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	245
56910 d1d986a97524 tuned GUI; wenzelm parents: 56909 diff changeset	246	private val apply_button = new Button("<html><b>Apply</b></html>") {
56865 168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	247	tooltip = "Apply to current context"
57000 c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	248	listenTo(keys)
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	249	reactions += {
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	250	case ButtonClicked(_) => apply_query()
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	251	case evt @ KeyPressed(_, Key.Enter, 0, _) =>
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	252	evt.peer.consume
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	253	apply_query()
c914618feef8 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus; wenzelm parents: 56918 diff changeset	254	}
56865 168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	255	}
168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	256
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	257	private val control_panel = Wrap_Panel()
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	258
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	259	def select: Unit =
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	260	{
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	261	control_panel.contents.clear()
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	262	control_panel.contents += query_label
30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	263	update_items().foreach(item => control_panel.contents += item.checkbox)
56883 38c6b70e5e53 common support for search field, which is actually a light-weight Highlighter; wenzelm parents: 56882 diff changeset	264	control_panel.contents ++=
57604 30885e25c6de support multiple selected print operations instead of slightly odd "menu"; wenzelm parents: 57044 diff changeset	265	List(process_indicator.component, apply_button,
57042 5576d22abf3c tuned signature; wenzelm parents: 57000 diff changeset	266	pretty_text_area.search_label, pretty_text_area.search_field, zoom)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	267	}
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	268
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	269	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	270	new TabbedPane.Page("Print Context", new BorderPanel {
59391 39a38657d16b tuned; wenzelm parents: 59286 diff changeset	271	layout(control_panel) = BorderPanel.Position.North
39a38657d16b tuned; wenzelm parents: 59286 diff changeset	272	layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	273	}, "Print information from context")
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	274	}
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	275
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	276
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	277	/* operations */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	278
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	279	private val operations = List(find_theorems, find_consts, print_operation)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	280
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	281	private val operations_pane = new TabbedPane
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	282	{
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	283	pages ++= operations.map(_.page)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	284	listenTo(selection)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	285	reactions += { case SelectionChanged(_) => select_operation() }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	286	}
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	287
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	288	private def get_operation(): Option[Query_Dockable.Operation] =
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	289	try { Some(operations(operations_pane.selection.index)) }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	290	catch { case _: IndexOutOfBoundsException => None }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	291
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	292	private def select_operation(): Unit =
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	293	{
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	294	for (op <- get_operation()) { op.select; op.query.requestFocus() }
77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	295	operations_pane.revalidate()
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	296	}
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	297
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	298	override def focusOnDefaultComponent(): Unit =
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	299	{
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73340 diff changeset	300	for (op <- get_operation()) op.query.requestFocus()
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	301	}
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	302
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	303	select_operation()
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	304	set_content(operations_pane)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	305
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 71525 diff changeset	306	override def detach_operation: Option[() => Unit] =
56918 a442dc6d244d clarified detach_operation: ignore empty output; wenzelm parents: 56911 diff changeset	307	get_operation() match {
a442dc6d244d clarified detach_operation: ignore empty output; wenzelm parents: 56911 diff changeset	308	case None => None
a442dc6d244d clarified detach_operation: ignore empty output; wenzelm parents: 56911 diff changeset	309	case Some(op) => op.pretty_text_area.detach_operation
a442dc6d244d clarified detach_operation: ignore empty output; wenzelm parents: 56911 diff changeset	310	}
56906 408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework; wenzelm parents: 56886 diff changeset	311
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	312
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	313	/* resize */
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	314
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	315	private def handle_resize(): Unit =
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57604 diff changeset	316	GUI_Thread.require {
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	317	for (op <- operations) {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	318	op.pretty_text_area.resize(
57044 042d6e58cb40 more uniform Font_Info.Zoom_Box; wenzelm parents: 57042 diff changeset	319	Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	320	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	321	}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	322
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	323	private val delay_resize =
71704 b9a5eb0f3b43 clarified modules; wenzelm parents: 71601 diff changeset	324	Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
52854 92932931bd82 more general Output.result: allow to update arbitrary properties; wenzelm parents: 52851 diff changeset	325
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	326	addComponentListener(new ComponentAdapter {
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	327	override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	328	override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	329	})
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	330
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	331
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	332	/* main */
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	333
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	334	private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	335	Session.Consumer[Session.Global_Options](getClass.getName) {
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 57604 diff changeset	336	case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	337	}
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	338
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	339	override def init(): Unit =
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	340	{
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	341	PIDE.session.global_options += main
52848 9489ca1d55dd some tracking of command location; wenzelm parents: 52846 diff changeset	342	handle_resize()
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	343	operations.foreach(op => op.query_operation.activate())
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	344	}
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	345
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 72215 diff changeset	346	override def exit(): Unit =
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	347	{
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	348	operations.foreach(op => op.query_operation.deactivate())
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	349	PIDE.session.global_options -= main
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	350	delay_resize.revoke()
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	351	}
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	352	}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	353

author	wenzelm
	Wed, 31 Mar 2021 17:15:54 +0200
changeset 73519	8f485a199874
parent 73367	77ef8bef0593
child 73987	fc363a3b690a
permissions	-rw-r--r--