isabelle: src/Tools/jEdit/src/isabelle_sidekick.scala@570ba266f5b5 (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
34426 81f93e0f13b4 renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser; wenzelm parents: 34417 diff changeset	8	package isabelle.jedit
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._
6111de7c916a adapted to Scala 2.8.0 Beta 1; wenzelm parents: 35004 diff changeset	12
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	13	import javax.swing.tree.DefaultMutableTreeNode
34701 80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag; wenzelm parents: 34669 diff changeset	14	import javax.swing.text.Position
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	15	import javax.swing.Icon
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	16
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	17	import org.gjt.sp.jedit.Buffer
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	18	import sidekick.{SideKickParser, SideKickParsedData, IAsset}
34701 80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag; wenzelm parents: 34669 diff changeset	19
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	20
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	21	object Isabelle_Sidekick
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	22	{
40477 780c27276593 tuned; wenzelm parents: 40475 diff changeset	23	def int_to_pos(offset: Text.Offset): Position =
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	24	new Position { def getOffset = offset; override def toString = offset.toString }
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	25
40477 780c27276593 tuned; wenzelm parents: 40475 diff changeset	26	class Asset(name: String, start: Text.Offset, end: Text.Offset) 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	27	{
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	28	protected var _name = 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	29	protected var _start = int_to_pos(start)
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	30	protected var _end = int_to_pos(end)
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	31	override def getIcon: Icon = null
53973 78bbe75c8437 enforce IsabelleText font for better symbol coverage, especially on Windows; wenzelm parents: 53281 diff changeset	32	override def getShortString: String =
53985 f6b7afa414f7 observe user preferences; wenzelm parents: 53973 diff changeset	33	"<html><span style=\"font-family: " + Rendering.font_family() + ";\">" +
f6b7afa414f7 observe user preferences; wenzelm parents: 53973 diff changeset	34	HTML.encode(_name) + "</span></html>"
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	35	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	36	override def getName: 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	37	override def setName(name: String) = _name = 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	38	override def getStart: Position = _start
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	39	override def setStart(start: Position) = _start = start
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	40	override def getEnd: Position = _end
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	41	override def setEnd(end: Position) = _end = end
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	42	override def toString = _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	43	}
51618 a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	44
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	45	def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	46	swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	47	{
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	48	for ((_, entry) <- tree.branches) {
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	49	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	50	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	51	parent.add(node)
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	52	}
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	53	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	54	}
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	55
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	56
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	57	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	58	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	59	override def supportsCompletion = false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	60
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	61
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	62	/* parsing */
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	63
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	64	@volatile protected var stopped = false
34503 7d0726f19d04 tuned whitespace; wenzelm parents: 34485 diff changeset	65	override def stop() = { 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	66
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	67	def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	68
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	69	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	70	{
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	71	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	72
38640 105d1f112da5 sporadic locking of jEdit buffer; wenzelm parents: 38577 diff changeset	73	// FIXME lock buffer (!??)
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	74	val data = new SideKickParsedData(buffer.getName)
34717 3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move; wenzelm parents: 34705 diff changeset	75	val root = data.root
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	76	data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
34475 f963335dbc6b implemented IsabelleSideKickParser.complete immler@in.tum.de parents: 34440 diff changeset	77
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	78	val syntax = Isabelle.mode_syntax(name)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	79	val ok =
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	80	if (syntax.isDefined) {
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	81	val ok = parser(buffer, syntax.get, data)
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	82	if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	83	else ok
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	84	}
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	85	else false
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	86	if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	87
34417 bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	88	data
bce2f2ea9819 misc tuning and adaption according to original IsabelleParser -- wenzelm parents: 34408 diff changeset	89	}
34393 f0e1608a774f basic tree structure for sidekick immler@in.tum.de parents: diff changeset	90	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	91
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	92
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	93	class Isabelle_Sidekick_Structure(
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	94	name: String,
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	95	node_name: Buffer => Option[Document.Node.Name])
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	96	extends Isabelle_Sidekick(name)
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	97	{
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	98	import Thy_Syntax.Structure
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	99
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	100	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	101	{
40477 780c27276593 tuned; wenzelm parents: 40475 diff changeset	102	def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	103	entry match {
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	104	case Structure.Block(name, body) =>
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	105	val node =
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	106	new DefaultMutableTreeNode(
40475 8a57ff2c2600 Sidekick block asset: show first line only; wenzelm parents: 40474 diff changeset	107	new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	108	(offset /: body)((i, e) =>
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	109	{
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	110	make_tree(i, e) foreach (nd => node.add(nd))
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	111	i + e.length
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	112	})
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	113	List(node)
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	114	case Structure.Atom(command)
40458 12c8c64203b3 treat main theory commands like headings, and nest anything else inside; wenzelm parents: 40455 diff changeset	115	if command.is_command && syntax.heading_level(command).isEmpty =>
40455 e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	116	val node =
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	117	new DefaultMutableTreeNode(
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	118	new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	119	List(node)
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	120	case _ => Nil
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	121	}
e035dad8eca2 default Sidekick parser based on section headings; wenzelm parents: 40452 diff changeset	122
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	123	node_name(buffer) match {
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	124	case Some(name) =>
49406 38db4832b210 somewhat more general JEdit_Lib; wenzelm parents: 48884 diff changeset	125	val text = JEdit_Lib.buffer_text(buffer)
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	126	val structure = Structure.parse(syntax, name, text)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	127	make_tree(0, structure) foreach (node => data.root.add(node))
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	128	true
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	129	case None => false
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	130	}
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	131	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	132	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	133
dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	134
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	135	class Isabelle_Sidekick_Default extends
54509 1f77110c94ef maintain document model for all files, with document view for theory only, and special blob for non-theory files; wenzelm parents: 53985 diff changeset	136	Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	137
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	138
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	139	class Isabelle_Sidekick_Options extends
54515 570ba266f5b5 clarified boundary cases of Document.Node.Name; wenzelm parents: 54509 diff changeset	140	Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
48718 73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	141
73e6c22e2d94 more structural parsing for minor modes; wenzelm parents: 48717 diff changeset	142
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	143	class Isabelle_Sidekick_Root extends
54515 570ba266f5b5 clarified boundary cases of Document.Node.Name; wenzelm parents: 54509 diff changeset	144	Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	145
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	146
53281 251e1a2aa792 clarified SideKick parser name, which serves as quasi "mode" here; wenzelm parents: 53274 diff changeset	147	class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	148	{
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	149	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	150	{
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	151	Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	152	case Some(snapshot) =>
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	153	val root = data.root
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	154	for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
51618 a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	155	Isabelle_Sidekick.swing_markup_tree(
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	156	snapshot.state.command_state(snapshot.version, command).markup, root,
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; wenzelm parents: 51493 diff changeset	157	(info: Text.Info[List[XML.Elem]]) =>
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	158	{
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	159	val range = info.range + command_start
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	160	val content = command.source(info.range).replace('\n', ' ')
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	161	val info_text =
51493 59d8a1031c00 allow fractional pretty margin -- avoid premature rounding; wenzelm parents: 50725 diff changeset	162	Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
59d8a1031c00 allow fractional pretty margin -- avoid premature rounding; wenzelm parents: 50725 diff changeset	163	.mkString
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	164
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	165	new DefaultMutableTreeNode(
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	166	new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	167	override def getShortString: String = content
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	168	override def getLongString: String = info_text
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	169	override def toString = quote(content) + " " + range.toString
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	170	})
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	171	})
48717 622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	172	}
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	173	true
622251b2b0f1 clarified Sidekick configuration, including minor modes; wenzelm parents: 47749 diff changeset	174	case None => false
36759 dc972354d77c tuned; wenzelm parents: 36738 diff changeset	175	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	176	}
dc972354d77c tuned; wenzelm parents: 36738 diff changeset	177	}
36738 dce592144219 support several sidekick parsers -- very basic default parser; wenzelm parents: 36737 diff changeset	178
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	179
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	180	class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	181	{
53274 1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	182	private val Heading1 = """^New in (.)\w$""".r
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View; wenzelm parents: 53233 diff changeset	183	private val Heading2 = """^\\\\w(.)\w\\\\w$""".r
52539 7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	184
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	185	private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	186	new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	187
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	188	override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	189	{
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	190	var offset = 0
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	191
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	192	for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	193	line match {
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	194	case Heading1(s) =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	195	data.root.add(make_node(Library.capitalize(s), offset, offset + line.length))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	196	case Heading2(s) =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	197	data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	198	.add(make_node(s, offset, offset + line.length))
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	199	case _ =>
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	200	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	201	offset += line.length + 1
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	202	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	203
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	204	true
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	205	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	206	}
7658f8d7b2dc minimal jedit mode for Isabelle NEWS; wenzelm parents: 51618 diff changeset	207

author	wenzelm
	Tue, 19 Nov 2013 12:57:56 +0100
changeset 54515	570ba266f5b5
parent 54509	1f77110c94ef
child 55432	9c53198dbb1c
permissions	-rw-r--r--