--- a/src/Pure/Isar/outer_syntax.scala Tue Oct 21 13:21:59 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Oct 21 13:56:42 2014 +0200
@@ -63,11 +63,11 @@
/* overall document structure */
sealed abstract class Document { def length: Int }
- case class Document_Block(val name: String, val body: List[Document]) extends Document
+ case class Document_Block(name: String, text: String, body: List[Document]) extends Document
{
val length: Int = (0 /: body)(_ + _.length)
}
- case class Document_Atom(val command: Command) extends Document
+ case class Document_Atom(command: Command) extends Document
{
def length: Int = command.length
}
@@ -301,14 +301,14 @@
def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
new mutable.ListBuffer[Outer_Syntax.Document]
- var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
- List((0, "", buffer()))
+ var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
+ List((0, Command.empty, buffer()))
@tailrec def close(level: Int => Boolean)
{
stack match {
- case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
- body2 += Outer_Syntax.Document_Block(name, body.toList)
+ case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
+ body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
stack = stack.tail
close(level)
case _ =>
@@ -326,7 +326,7 @@
heading_level(command) match {
case Some(i) =>
close(_ > i)
- stack = (i + 1, command.source, buffer()) :: stack
+ stack = (i + 1, command, buffer()) :: stack
case None =>
}
stack.head._3 += Outer_Syntax.Document_Atom(command)
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Tue Oct 21 13:21:59 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Tue Oct 21 13:56:42 2014 +0200
@@ -231,9 +231,8 @@
{
override def supportsCompletion = false
- private class Asset(
- label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
- extends Isabelle_Sidekick.Asset(label, start, stop) {
+ private class Asset(label: String, label_html: String, range: Text.Range, source: String)
+ extends Isabelle_Sidekick.Asset(label, range) {
override def getShortString: String = label_html
override def getLongString: String = source
}
@@ -252,7 +251,8 @@
val label = kind + (if (name == "") "" else " " + name)
val label_html =
"<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
- val asset = new Asset(label, label_html, offset, offset + source.size, source)
+ val range = Text.Range(offset, offset + source.size)
+ val asset = new Asset(label, label_html, range, source)
data.root.add(new DefaultMutableTreeNode(asset))
}
offset += source.size
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Oct 21 13:21:59 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Oct 21 13:56:42 2014 +0200
@@ -30,15 +30,17 @@
data
}
- class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
+ class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
{
- protected var _name = name
- protected var _start = int_to_pos(start)
- protected var _end = int_to_pos(end)
+ protected var _name = text
+ protected var _start = int_to_pos(range.start)
+ protected var _end = int_to_pos(range.stop)
override def getIcon: Icon = null
override def getShortString: String =
"<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
- HTML.encode(_name) + "</span></html>"
+ (if (keyword != "" && _name.startsWith(keyword))
+ "<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
+ else HTML.encode(_name)) + "</span></html>"
override def getLongString: String = _name
override def getName: String = _name
override def setName(name: String) = _name = name
@@ -49,6 +51,8 @@
override def toString: String = _name
}
+ class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
+
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
{
@@ -108,10 +112,11 @@
{
(offset /: documents) { case (i, document) =>
document match {
- case Outer_Syntax.Document_Block(name, body) =>
+ case Outer_Syntax.Document_Block(name, text, body) =>
+ val range = Text.Range(i, i + document.length)
val node =
new DefaultMutableTreeNode(
- new Isabelle_Sidekick.Asset(Library.first_line(name), i, i + document.length))
+ new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
parent.add(node)
make_tree(node, i, body)
case _ =>
@@ -170,7 +175,7 @@
.mkString
new DefaultMutableTreeNode(
- new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
+ new Isabelle_Sidekick.Asset(command.toString, range) {
override def getShortString: String = content
override def getLongString: String = info_text
override def toString: String = quote(content) + " " + range.toString
@@ -190,7 +195,7 @@
private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
- new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
+ new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{