isabelle: src/Tools/jEdit/src/query_dockable.scala@dc3ba749d3b8 (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._
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	11
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	12	import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	13	import javax.swing.{JComponent, JTextField}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	14
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	15	import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	16	ComboBox, TabbedPane, BorderPanel}
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	17	import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	18
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	19	import org.gjt.sp.jedit.View
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	20
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	21
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	22	object Query_Dockable
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	23	{
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	24	private abstract class Operation(view: View)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	25	{
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	26	val pretty_text_area = new Pretty_Text_Area(view)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	27	def query_operation: Query_Operation[View]
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	28	def query: JComponent
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	29	def select: Unit
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	30	def page: TabbedPane.Page
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	31	}
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
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	34	class Query_Dockable(view: View, position: String) extends Dockable(view, position)
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	35	{
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	36	/* common GUI components */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	37
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	38	private var zoom_factor = 100
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	39	private val zoom =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	40	new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	41	{
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	42	tooltip = "Zoom factor for output font size"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	43	}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	44
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	45	private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	46	new Completion_Popup.History_Text_Field(property)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	47	{
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	48	override def processKeyEvent(evt: KeyEvent)
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	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	51	super.processKeyEvent(evt)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	52	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	53	{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	54	setColumns(40)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	55	setToolTipText(tooltip)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	56	setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	57	}
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	58
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	59
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	60	/* consume status */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	61
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	62	def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	63	{
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	64	status match {
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	65	case Query_Operation.Status.WAITING =>
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	66	process_indicator.update("Waiting for evaluation of context ...", 5)
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	67	case Query_Operation.Status.RUNNING =>
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	68	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	69	case Query_Operation.Status.FINISHED =>
52935 6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	70	process_indicator.update(null, 0)
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	71	}
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	72	}
6fc13c31c775 more abstract consume_status operation; wenzelm parents: 52886 diff changeset	73
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	74
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	75	/* find theorems */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	76
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	77	private val find_theorems = new Query_Dockable.Operation(view)
56757 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	/* query */
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	private val process_indicator = new Process_Indicator
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	82
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	83	val query_operation =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	84	new Query_Operation(PIDE.editor, view, "find_theorems",
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	85	consume_status(process_indicator, _),
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	86	(snapshot, results, body) =>
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	87	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	88
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	89	private def apply_query()
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	90	{
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	91	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	92	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	93
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	94	private val query_label = new Label("Find:") {
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	95	tooltip =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	96	GUI.tooltip_lines(
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	97	"Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
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
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	100	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	101
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	102
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	103	/* GUI page */
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	104
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	105	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	106	tooltip = "Limit of displayed results"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	107	verifier = (s: String) =>
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	108	s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	109	listenTo(keys)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	110	reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
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
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	113	private val allow_dups = new CheckBox("Duplicates") {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	114	tooltip = "Show all versions of matching theorems"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	115	selected = false
56911 dc3ba749d3b8 tuned GUI; wenzelm parents: 56910 diff changeset	116	reactions += { case ButtonClicked(_) => apply_query() }
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	117	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	118
56910 d1d986a97524 tuned GUI; wenzelm parents: 56909 diff changeset	119	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	120	tooltip = "Find theorems meeting specified criteria"
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	121	reactions += { case ButtonClicked(_) => apply_query() }
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	122	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	123
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	124	private val control_panel =
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	125	new Wrap_Panel(Wrap_Panel.Alignment.Right)(
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	126	query_label, Component.wrap(query), limit, allow_dups,
56907 0f3c375fd27c enable "PIDE" docking framework by default, and rely on its "Detach" menu item; wenzelm parents: 56906 diff changeset	127	process_indicator.component, apply_button,
56886 87ebb99786ed tuned GUI layout; wenzelm parents: 56883 diff changeset	128	pretty_text_area.search_label, pretty_text_area.search_pattern)
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	129
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	130	def select { control_panel.contents += zoom }
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	131
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	132	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	133	new TabbedPane.Page("Find Theorems", new BorderPanel {
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	134	add(control_panel, BorderPanel.Position.North)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	135	add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	136	}, apply_button.tooltip)
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
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	139
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	140	/* find consts */
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	141
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	142	private val find_consts = new Query_Dockable.Operation(view)
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	143	{
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	144	/* query */
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	145
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	146	private val process_indicator = new Process_Indicator
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	147
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	148	val query_operation =
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	149	new Query_Operation(PIDE.editor, view, "find_consts",
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	150	consume_status(process_indicator, _),
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	151	(snapshot, results, body) =>
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	152	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	153
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	154	private def apply_query()
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	155	{
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 =
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	174	new Wrap_Panel(Wrap_Panel.Alignment.Right)(
56907 0f3c375fd27c enable "PIDE" docking framework by default, and rely on its "Detach" menu item; wenzelm parents: 56906 diff changeset	175	query_label, Component.wrap(query), process_indicator.component, apply_button,
56886 87ebb99786ed tuned GUI layout; wenzelm parents: 56883 diff changeset	176	pretty_text_area.search_label, pretty_text_area.search_pattern)
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	177
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	178	def select { control_panel.contents += zoom }
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	179
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	180	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	181	new TabbedPane.Page("Find Constants", new BorderPanel {
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	182	add(control_panel, BorderPanel.Position.North)
56758 d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	183	add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	184	}, apply_button.tooltip)
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	185	}
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	186
d203b9c400a2 PIDE support for find_consts; wenzelm parents: 56757 diff changeset	187
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	188	/* print operation */
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	189
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	190	private val print_operation = new Query_Dockable.Operation(view)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	191	{
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	192	/* query */
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	193
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	194	private val process_indicator = new Process_Indicator
a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	195
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	196	val query_operation =
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	197	new Query_Operation(PIDE.editor, view, "print_operation",
a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	198	consume_status(process_indicator, _),
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	199	(snapshot, results, body) =>
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	200	pretty_text_area.update(snapshot, results, Pretty.separate(body)))
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	201
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	202	private def apply_query()
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	203	{
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	204	query_operation.apply_query(List(selector.selection.item))
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	205	}
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	206
56866 c4512e94e15c tuned GUI; wenzelm parents: 56865 diff changeset	207	private val query_label = new Label("Print:")
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	208	def query: JComponent = apply_button.peer
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	209
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	210
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	211	/* items */
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	212
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	213	case class Item(name: String, description: String)
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	214
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	215	class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	216	extends ListView.Renderer[String]
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	217	{
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	218	def componentFor(list: ListView[_],
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	219	selected: Boolean, focused: Boolean, item: String, index: Int) =
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	220	{
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	221	val component = old_renderer.componentFor(list, selected, focused, item, index)
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	222	try { component.tooltip = items(index).description }
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	223	catch { case _: IndexOutOfBoundsException => }
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	224	component
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	225	}
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	226	}
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	227
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	228	private var selector_item: Option[String] = None
6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	229	private var selector = new ComboBox[String](Nil)
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	230
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	231	private def set_selector()
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	232	{
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	233	val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	234
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	235	selector =
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	236	new ComboBox(items.map(_.name)) {
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	237	selector_item.foreach(item => selection.item = item)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	238	listenTo(selection)
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	239	reactions += {
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	240	case SelectionChanged(_) =>
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	241	selector_item = Some(selection.item)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	242	apply_query()
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	243	}
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	244	}
56882 6d4b2f8f010c clarified GUI focus; wenzelm parents: 56881 diff changeset	245	selector.renderer = new Renderer(selector.renderer, items)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	246	}
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	247	set_selector()
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	248
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	249
1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	250	/* GUI page */
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	251
56910 d1d986a97524 tuned GUI; wenzelm parents: 56909 diff changeset	252	private val apply_button = new Button("<html><b>Apply</b></html>") {
56865 168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	253	tooltip = "Apply to current context"
168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	254	reactions += { case ButtonClicked(_) => apply_query() }
168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	255	}
168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	256
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	257	private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	258
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	259	def select
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	260	{
56872 1435f0c771dc some complication with ListView.Renderer to get tooltips; wenzelm parents: 56866 diff changeset	261	set_selector()
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	262	control_panel.contents.clear
56883 38c6b70e5e53 common support for search field, which is actually a light-weight Highlighter; wenzelm parents: 56882 diff changeset	263	control_panel.contents ++=
56909 a1557dc7f589 tuned GUI; wenzelm parents: 56907 diff changeset	264	List(query_label, selector, process_indicator.component, apply_button,
56886 87ebb99786ed tuned GUI layout; wenzelm parents: 56883 diff changeset	265	pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	266	}
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	val page =
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	269	new TabbedPane.Page("Print Context", new BorderPanel {
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	270	add(control_panel, BorderPanel.Position.North)
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	271	add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	272	}, "Print information from context")
0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	273	}
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
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	276	/* operations */
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	277
56864 0446c7ac2e32 support print operations as asynchronous query; wenzelm parents: 56759 diff changeset	278	private val operations = List(find_theorems, find_consts, print_operation)
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	279
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	280	private val operations_pane = new TabbedPane
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	281	{
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	282	pages ++= operations.map(_.page)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	283	listenTo(selection)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	284	reactions += { case SelectionChanged(_) => select_operation() }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	285	}
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	286
56879 ee2b61f37ad9 renamed "Find" to "Query", with more general operations; wenzelm parents: 56872 diff changeset	287	private def get_operation(): Option[Query_Dockable.Operation] =
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	288	try { Some(operations(operations_pane.selection.index)) }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	289	catch { case _: IndexOutOfBoundsException => None }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	290
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	291	private def select_operation() {
56865 168766e28f5e more decisive change of focus; wenzelm parents: 56864 diff changeset	292	for (op <- get_operation()) { op.select; op.query.requestFocus }
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	293	operations_pane.revalidate
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	294	}
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	295
56759 790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	296	override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	297
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	298	select_operation()
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	299	set_content(operations_pane)
790f7562cd0e proper handling of shared zoom component: update layout dynamically; wenzelm parents: 56758 diff changeset	300
56906 408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework; wenzelm parents: 56886 diff changeset	301	override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework; wenzelm parents: 56886 diff changeset	302
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	303
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	304	/* resize */
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	305
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	306	private def handle_resize(): Unit =
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	307	Swing_Thread.require {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	308	for (op <- operations) {
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	309	op.pretty_text_area.resize(
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	310	Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	311	}
d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	312	}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	313
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	314	private val delay_resize =
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	315	Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
52854 92932931bd82 more general Output.result: allow to update arbitrary properties; wenzelm parents: 52851 diff changeset	316
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	317	addComponentListener(new ComponentAdapter {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	318	override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52864 diff changeset	319	})
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	320
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	321
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	322	/* main */
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	323
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	324	private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	325	Session.Consumer[Session.Global_Options](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	326	case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	327	}
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	328
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	329	override def init()
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	330	{
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	331	PIDE.session.global_options += main
52848 9489ca1d55dd some tracking of command location; wenzelm parents: 52846 diff changeset	332	handle_resize()
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	333	operations.foreach(op => op.query_operation.activate())
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	334	}
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	335
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	336	override def exit()
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	337	{
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	338	operations.foreach(op => op.query_operation.deactivate())
56715 52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread; wenzelm parents: 56662 diff changeset	339	PIDE.session.global_options -= main
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	340	delay_resize.revoke()
82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	341	}
56757 d6fdf08282f3 some rearrangements to support multiple find operations; wenzelm parents: 56751 diff changeset	342	}
52846 82ac963c68cb dockable window for "find" dialog (GUI only); wenzelm parents: diff changeset	343

author	wenzelm
	Thu, 08 May 2014 15:30:28 +0200
changeset 56911	dc3ba749d3b8
parent 56910	d1d986a97524
child 56918	a442dc6d244d
permissions	-rw-r--r--