# HG changeset patch # User wenzelm # Date 1413892602 -7200 # Node ID c680f181b32efe7d8a82bb500d65d56e34ab69b9 # Parent 68c2cbe2fd3a48c398780ce6eaf87aa9db3e91dd tuned rendering; diff -r 68c2cbe2fd3a -r c680f181b32e src/Pure/Isar/outer_syntax.scala --- 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) diff -r 68c2cbe2fd3a -r c680f181b32e src/Tools/jEdit/src/bibtex_jedit.scala --- 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 = "" + kind + "" + (if (name == "") "" else " " + name) + "" - 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 diff -r 68c2cbe2fd3a -r c680f181b32e src/Tools/jEdit/src/isabelle_sidekick.scala --- 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.encode(_name) + "" + (if (keyword != "" && _name.startsWith(keyword)) + "" + HTML.encode(keyword) + "" + HTML.encode(_name.substring(keyword.length)) + else HTML.encode(_name)) + "" 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 = {