isabelle: src/Tools/jEdit/src/documentation_dockable.scala@9bd948666e8a (annotated)

52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	1	/* Title: Tools/jEdit/src/documentation_dockable.scala
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	2	Author: Makarius
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	3
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	4	Dockable window for Isabelle documentation.
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	5	*/
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	6
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	7	package isabelle.jedit
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	8
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	9
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	10	import isabelle._
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	11
60847 239d7714392b tuned; wenzelm parents: 60292 diff changeset	12	import java.awt.Dimension
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	13	import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
60847 239d7714392b tuned; wenzelm parents: 60292 diff changeset	14	import javax.swing.{JTree, JScrollPane}
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	15	import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	16
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	17	import org.gjt.sp.jedit.{View, OperatingSystem}
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	18
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	19
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	20	class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75115 diff changeset	21	private val doc_contents = Doc.contents()
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	22
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	23	private case class Node(string: String, entry: Doc.Entry) {
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	24	override def toString: String = string
52541 97c950217d7f quick access to release notes (imitating website/documentation.html); wenzelm parents: 52447 diff changeset	25	}
97c950217d7f quick access to release notes (imitating website/documentation.html); wenzelm parents: 52447 diff changeset	26
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	27	private val root = new DefaultMutableTreeNode
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75115 diff changeset	28	for (section <- doc_contents.sections) {
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	29	root.add(new DefaultMutableTreeNode(section.title))
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	30	section.entries.foreach(
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	31	{
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	32	case entry @ Doc.Doc(name, title, _) =>
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	33	val string = "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	34	root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	35	.add(new DefaultMutableTreeNode(Node(string, entry)))
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	36	case entry @ Doc.Text_File(name: String, _) =>
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	37	root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	38	.add(new DefaultMutableTreeNode(Node(name, entry)))
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	39	})
52541 97c950217d7f quick access to release notes (imitating website/documentation.html); wenzelm parents: 52447 diff changeset	40	}
97c950217d7f quick access to release notes (imitating website/documentation.html); wenzelm parents: 52447 diff changeset	41
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	42	private val tree = new JTree(root)
60292 ba3c716144dd cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows; wenzelm parents: 59390 diff changeset	43	tree.setRowHeight(0)
60847 239d7714392b tuned; wenzelm parents: 60292 diff changeset	44	tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
54687 795f8d3e06c9 no keyboard control -- avoid confusion about meaning of selection; wenzelm parents: 54686 diff changeset	45
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 71525 diff changeset	46	override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
54687 795f8d3e06c9 no keyboard control -- avoid confusion about meaning of selection; wenzelm parents: 54686 diff changeset	47
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	48	private def action(node: DefaultMutableTreeNode): Unit = {
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	49	node.getUserObject match {
75120 488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	50	case Node(_, Doc.Doc(_, _, path)) =>
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	51	PIDE.editor.goto_doc(view, path)
488c7e8923b2 clarified pdf path; wenzelm parents: 75118 diff changeset	52	case Node(_, Doc.Text_File(_, path)) =>
66082 2d12a730a380 clarified modules; wenzelm parents: 65246 diff changeset	53	PIDE.editor.goto_file(true, view, File.platform_path(path))
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	54	case _ =>
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	55	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	56	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	57
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	58	tree.addKeyListener(new KeyAdapter {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	59	override def keyPressed(e: KeyEvent): Unit = {
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	60	if (e.getKeyCode == KeyEvent.VK_ENTER) {
75807 b0394e7d43ea tuned signature, following hints by IntelliJ IDEA; wenzelm parents: 75393 diff changeset	61	e.consume()
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	62	val path = tree.getSelectionPath
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	63	if (path != null) {
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	64	path.getLastPathComponent match {
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	65	case node: DefaultMutableTreeNode => action(node)
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	66	case _ =>
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	67	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	68	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	69	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	70	}
c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	71	})
54686 070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	72	tree.addMouseListener(new MouseAdapter {
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 75120 diff changeset	73	override def mouseClicked(e: MouseEvent): Unit = {
54686 070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	74	val click = tree.getPathForLocation(e.getX, e.getY)
070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	75	if (click != null && e.getClickCount == 1) {
070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	76	(click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	77	case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
57920 c1953856cfca clarified focus and key handling -- more like SideKick; wenzelm parents: 57912 diff changeset	78	action(node)
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	79	case _ =>
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	80	}
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	81	}
54686 070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	82	}
070d5e856798 directly react on click, assuming that document view operation is mostly idempotent; wenzelm parents: 53177 diff changeset	83	})
56423 c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	84
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	85	{
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	86	var expand = true
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	87	var visible = 0
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	88	var row = 0
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	89	def make_visible(): Unit = { visible += 1; tree.expandRow(row) }
75118 6fd8e482c9ce clarified signature; wenzelm parents: 75115 diff changeset	90	for (section <- doc_contents.sections) {
75115 c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	91	expand = section.important
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	92	make_visible()
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	93	row += 1
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	94	for (_ <- section.entries) {
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	95	if (expand) make_visible()
c212435866d6 clarified signature: more explicit section structure; wenzelm parents: 75114 diff changeset	96	row += 1
56423 c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	97	}
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	98	}
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	99	tree.setRootVisible(false)
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	100	tree.setVisibleRowCount(visible)
c2f52824dbb2 explicit indication of important doc sections ("!"), which are expanded in the tree view; wenzelm parents: 56422 diff changeset	101	}
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	102
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	103	private val tree_view = new JScrollPane(tree)
60849 6e49311ef842 tuned; wenzelm parents: 60847 diff changeset	104	tree_view.setMinimumSize(new Dimension(200, 50))
52445 18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	105
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	106	set_content(tree_view)
18a720984855 dockable window for Isabelle documentation; wenzelm parents: diff changeset	107	}

author	wenzelm
	Mon, 24 Oct 2022 20:24:34 +0200
changeset 76370	9bd948666e8a
parent 75807	b0394e7d43ea
child 81319	a0b25f94c74a
permissions	-rw-r--r--