isabelle: src/Tools/jEdit/jedit_main/isabelle_sidekick.scala@f741d55a81e5 (annotated)

43282 5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory; wenzelm parents: 40792 diff changeset	1	/* Title: Tools/jEdit/src/isabelle_sidekick.scala
36760 b82a698ef6c9 tuned headers; wenzelm parents: 36759 diff changeset	2	Author: Fabian Immler, TU Munich
b82a698ef6c9 tuned headers; wenzelm parents: 36759 diff changeset	3	Author: Makarius
b82a698ef6c9 tuned headers; wenzelm parents: 36759 diff changeset	4
b82a698ef6c9 tuned headers; wenzelm parents: 36759 diff changeset	5	SideKick parsers for Isabelle proof documents.
b82a698ef6c9 tuned headers; wenzelm parents: 36759 diff changeset	6	*/
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	7
73987 fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	8	package isabelle.jedit_main
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	9
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	10
36015 6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 35004 diff changeset	11	import isabelle._
73987 fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	12	import isabelle.jedit._
36015 6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 35004 diff changeset	13
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	14	import javax.swing.tree.DefaultMutableTreeNode
34701 80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag; wenzelm parents: 34669 diff changeset	15	import javax.swing.text.Position
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	16	import javax.swing.Icon
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	17
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	18	import org.gjt.sp.jedit.Buffer
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	19	import sidekick.{SideKickParser, SideKickParsedData, IAsset}
34701 80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag; wenzelm parents: 34669 diff changeset	20
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	21
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	22	object Isabelle_Sidekick
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	23	{
40477 780c27276593 tuned; wenzelm parents: 40475 diff changeset	24	def int_to_pos(offset: Text.Offset): Position =
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	25	new Position {
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	26	def getOffset: Text.Offset = offset
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	27	override def toString: String = offset.toString
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	28	}
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	29
58526 f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	30	def root_data(buffer: Buffer): SideKickParsedData =
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	31	{
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	32	val data = new SideKickParsedData(buffer.getName)
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	33	data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	34	data
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	35	}
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	36
58747 c680f181b32e tuned rendering; wenzelm parents: 58743 diff changeset	37	class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	38	{
69377 81ae5893c556 use Isabelle fonts for all GUI look-and-feels; wenzelm parents: 69358 diff changeset	39	private val css = GUI.imitate_font_css(GUI.label_font())
59183 ec83638b6bfb imitate font more carefully: err on smaller size; wenzelm parents: 59091 diff changeset	40
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	41	protected var _name: String = text
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	42	protected var _start: Position = int_to_pos(range.start)
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	43	protected var _end: Position = int_to_pos(range.stop)
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	44	override def getIcon: Icon = null
53973 78bbe75c8437 enforce IsabelleText font for better symbol coverage, especially on Windows; wenzelm parents: 53281 diff changeset	45	override def getShortString: String =
59933 07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	46	{
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	47	val n = keyword.length
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	48	val s =
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	49	_name.indexOf(keyword) match {
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	50	case i if i >= 0 && n > 0 =>
62113 16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 61871 diff changeset	51	HTML.output(_name.substring(0, i)) +
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 61871 diff changeset	52	"<b>" + HTML.output(keyword) + "</b>" +
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 61871 diff changeset	53	HTML.output(_name.substring(i + n))
16de2a9b5b3d tuned -- according to ML version; wenzelm parents: 61871 diff changeset	54	case _ => HTML.output(_name)
59933 07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	55	}
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	56	"<html><span style=\"" + css + "\">" + s + "</span></html>"
07a7544c0535 allow prefix before keyword, notably 'private'; wenzelm parents: 59286 diff changeset	57	}
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	58	override def getLongString: String = _name
45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	59	override def getName: String = _name
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	60	override def setName(name: String): Unit = _name = name
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	61	override def getStart: Position = _start
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	62	override def setStart(start: Position): Unit = _start = start
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	63	override def getEnd: Position = _end
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	64	override def setEnd(end: Position): Unit = _end = end
57912 dd9550f84106 tuned; wenzelm parents: 57904 diff changeset	65	override def toString: String = _name
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	66	}
51618 a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	67
58747 c680f181b32e tuned rendering; wenzelm parents: 58743 diff changeset	68	class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
c680f181b32e tuned rendering; wenzelm parents: 58743 diff changeset	69
51618 a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	70	def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 71601 diff changeset	71	swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
51618 a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	72	{
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	73	for ((_, entry) <- tree.branches) {
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	74	val node = swing_node(Text.Info(entry.range, entry.markup))
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	75	swing_markup_tree(entry.subtree, node, swing_node)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	76	parent.add(node)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	77	}
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	78	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	79	}
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	80
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	81
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	82	class Isabelle_Sidekick(name: String) extends SideKickParser(name)
34625 799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); wenzelm parents: 34612 diff changeset	83	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	84	override def supportsCompletion = false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	85
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	86
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	87	/* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	88
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	89	@volatile protected var stopped = false
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	90	override def stop(): Unit = { stopped = true }
34401 44241a37b74a structure of markup-tree in scala, keep track of swing-nodes in background immler@in.tum.de parents: 34393 diff changeset	91
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	92	def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	93
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	94	def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
34625 799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); wenzelm parents: 34612 diff changeset	95	{
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	96	stopped = false
34625 799a40faa4f1 completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file); wenzelm parents: 34612 diff changeset	97
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38577 diff changeset	98	// FIXME lock buffer (!??)
58526 f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	99	val data = Isabelle_Sidekick.root_data(buffer)
60272 4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch; wenzelm parents: 59933 diff changeset	100	val syntax = Isabelle.buffer_syntax(buffer)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	101	val ok =
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	102	if (syntax.isDefined) {
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	103	val ok = parser(buffer, syntax.get, data)
58526 f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	104	if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	105	else ok
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	106	}
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	107	else false
58526 f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	108	if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	109
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	110	data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	111	}
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	112	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	113
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	114
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	115	class Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	116	name: String,
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	117	node_name: Buffer => Option[Document.Node.Name],
fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	118	parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	119	extends Isabelle_Sidekick(name)
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	120	{
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	121	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	122	{
58743 c07a59140fee clarified tree root; wenzelm parents: 58707 diff changeset	123	def make_tree(
c07a59140fee clarified tree root; wenzelm parents: 58707 diff changeset	124	parent: DefaultMutableTreeNode,
c07a59140fee clarified tree root; wenzelm parents: 58707 diff changeset	125	offset: Text.Offset,
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 71601 diff changeset	126	documents: List[Document_Structure.Document]): Unit =
58743 c07a59140fee clarified tree root; wenzelm parents: 58707 diff changeset	127	{
73359 d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	128	documents.foldLeft(offset) {
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	129	case (i, document) =>
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	130	document match {
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	131	case Document_Structure.Block(name, text, body) =>
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	132	val range = Text.Range(i, i + document.length)
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	133	val node =
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	134	new DefaultMutableTreeNode(
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	135	new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	136	parent.add(node)
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	137	make_tree(node, i, body)
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	138	case _ =>
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	139	}
d8a0e996614b tuned --- fewer warnings; wenzelm parents: 73358 diff changeset	140	i + document.length
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	141	}
58743 c07a59140fee clarified tree root; wenzelm parents: 58707 diff changeset	142	}
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	143
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	144	node_name(buffer) match {
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	145	case Some(name) =>
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	146	make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	147	true
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	148	case None =>
fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	149	false
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	150	}
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	151	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	152	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	153
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	154	class Isabelle_Sidekick_Default extends
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	155	Isabelle_Sidekick_Structure("isabelle",
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	156	PIDE.resources.theory_node_name, Document_Structure.parse_sections)
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	157
fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	158	class Isabelle_Sidekick_Context extends
fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	159	Isabelle_Sidekick_Structure("isabelle-context",
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	160	PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	161
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	162	class Isabelle_Sidekick_Options extends
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	163	Isabelle_Sidekick_Structure("isabelle-options",
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	164	_ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	165
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	166	class Isabelle_Sidekick_Root extends
63606 fc3a23763617 support for context block structure in Sidekick; wenzelm parents: 63605 diff changeset	167	Isabelle_Sidekick_Structure("isabelle-root",
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	168	_ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	169
63610 4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	170	class Isabelle_Sidekick_ML extends
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	171	Isabelle_Sidekick_Structure("isabelle-ml",
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	172	buffer => Some(PIDE.resources.node_name(buffer)),
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	173	(_, _, text) => Document_Structure.parse_ml_sections(false, text))
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	174
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	175	class Isabelle_Sidekick_SML extends
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	176	Isabelle_Sidekick_Structure("isabelle-sml",
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	177	buffer => Some(PIDE.resources.node_name(buffer)),
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	178	(_, _, text) => Document_Structure.parse_ml_sections(true, text))
4b40b8196dc7 Sidekick parser for isabelle-ml and sml mode; wenzelm parents: 63606 diff changeset	179
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	180
53281 251e1a2aa792 clarified SideKick parser name, which serves as quasi "mode" here; wenzelm parents: 53274 diff changeset	181	class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	182	{
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	183	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	184	{
55513 6d21415e3909 recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread; wenzelm parents: 55432 diff changeset	185	val opt_snapshot =
64813 7283f41d05ab manage buffer models as explicit global state; wenzelm parents: 63610 diff changeset	186	Document_Model.get(buffer) match {
73367 77ef8bef0593 clarified signature --- fewer warnings; wenzelm parents: 73359 diff changeset	187	case Some(model) if model.is_theory => Some(model.snapshot())
60272 4f72b00d9952 no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch; wenzelm parents: 59933 diff changeset	188	case _ => None
55513 6d21415e3909 recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread; wenzelm parents: 55432 diff changeset	189	}
6d21415e3909 recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread; wenzelm parents: 55432 diff changeset	190	opt_snapshot match {
6d21415e3909 recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread; wenzelm parents: 55432 diff changeset	191	case Some(snapshot) =>
56373 0605d90be6fc tuned signature -- more explicit iterator terminology; wenzelm parents: 56301 diff changeset	192	for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
55650 349afd0fa0c4 tuned signature; wenzelm parents: 55513 diff changeset	193	val markup =
56301 1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query; wenzelm parents: 56299 diff changeset	194	snapshot.state.command_markup(
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query; wenzelm parents: 56299 diff changeset	195	snapshot.version, command, Command.Markup_Index.markup,
56743 81370dfadb1d tuned signature; wenzelm parents: 56609 diff changeset	196	command.range, Markup.Elements.full)
58526 f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	197	Isabelle_Sidekick.swing_markup_tree(markup, data.root,
f05ccce3eca2 SideKick parser for bibtex entries; wenzelm parents: 57912 diff changeset	198	(info: Text.Info[List[XML.Elem]]) =>
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	199	{
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	200	val range = info.range + command_start
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	201	val content = command.source(info.range).replace('\n', ' ')
65130 695930882487 tuned; wenzelm parents: 64813 diff changeset	202	val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	203
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	204	new DefaultMutableTreeNode(
58747 c680f181b32e tuned rendering; wenzelm parents: 58743 diff changeset	205	new Isabelle_Sidekick.Asset(command.toString, range) {
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	206	override def getShortString: String = content
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	207	override def getLongString: String = info_text
57912 dd9550f84106 tuned; wenzelm parents: 57904 diff changeset	208	override def toString: String = quote(content) + " " + range.toString
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	209	})
40452 45e7c2889d2f misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); wenzelm parents: 39624 diff changeset	210	})
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	211	}
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	212	true
55513 6d21415e3909 recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread; wenzelm parents: 55432 diff changeset	213	case None => false
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	214	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	215	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	216	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	217
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	218
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	219	class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	220	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	221	private val Heading1 = """^New in (.)\w$""".r
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	222	private val Heading2 = """^\\\\w(.)\w\\\\w$""".r
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	223
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	224	private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
58747 c680f181b32e tuned rendering; wenzelm parents: 58743 diff changeset	225	new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	226
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	227	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	228	{
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	229	var offset = 0
58542 19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	230	var end_offset = 0
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	231
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	232	var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	233	var start2: Option[(Int, String)] = None
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	234
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	235	def close1(): Unit =
58542 19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	236	start1 match {
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	237	case Some((start_offset, s, body)) =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	238	val node = make_node(s, start_offset, end_offset)
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	239	body.foreach(node.add(_))
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	240	data.root.add(node)
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	241	start1 = None
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	242	case None =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	243	}
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	244
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	245	def close2(): Unit =
58542 19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	246	start2 match {
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	247	case Some((start_offset, s)) =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	248	start1 match {
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	249	case Some((start_offset1, s1, body)) =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	250	val node = make_node(s, start_offset, end_offset)
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	251	start1 = Some((start_offset1, s1, body :+ node))
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	252	case None =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	253	}
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	254	start2 = None
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	255	case None =>
19e062fbfea0 more advanced NEWS tree structure and folding; wenzelm parents: 58539 diff changeset	256	}
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	257
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	258	for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	259	line match {
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	260	case Heading1(s) => close2(); close1(); start1 = Some((offset, s, Vector()))
c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	261	case Heading2(s) => close2(); start2 = Some((offset, s))
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	262	case _ =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	263	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	264	offset += line.length + 1
71601 97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA; wenzelm parents: 69377 diff changeset	265	if (!line.forall(Character.isSpaceChar)) end_offset = offset
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	266	}
74037 c13198575f75 tuned --- based on hints by IntelliJ IDEA; wenzelm parents: 73987 diff changeset	267	if (!stopped) { close2(); close1() }
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	268
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	269	true
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	270	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	271	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	272
73987 fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	273	class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	274	{
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	275	override def supportsCompletion = false
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	276
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	277	private class Asset(label: String, label_html: String, range: Text.Range, source: String)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	278	extends Isabelle_Sidekick.Asset(label, range) {
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	279	override def getShortString: String = label_html
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	280	override def getLongString: String = source
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	281	}
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	282
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	283	def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	284	{
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	285	val data = Isabelle_Sidekick.root_data(buffer)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	286
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	287	try {
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	288	var offset = 0
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	289	for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	290	val kind = chunk.kind
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	291	val name = chunk.name
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	292	val source = chunk.source
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	293	if (kind != "") {
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	294	val label = kind + (if (name == "") "" else " " + name)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	295	val label_html =
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	296	"<html><b>" + HTML.output(kind) + "</b>" +
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	297	(if (name == "") "" else " " + HTML.output(name)) + "</html>"
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	298	val range = Text.Range(offset, offset + source.length)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	299	val asset = new Asset(label, label_html, range, source)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	300	data.root.add(new DefaultMutableTreeNode(asset))
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	301	}
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	302	offset += source.length
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	303	}
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	304	data
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	305	}
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	306	catch { case ERROR(msg) => Output.warning(msg); null }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	307	}
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit; wenzelm parents: 73367 diff changeset	308	}

author	blanchet
	Mon, 31 Jan 2022 16:09:23 +0100
changeset 75025	f741d55a81e5
parent 74037	c13198575f75
child 75393	87ebf5a50283
permissions	-rw-r--r--