tuned rendering;
authorwenzelm
Tue Oct 21 13:56:42 2014 +0200 (2014-10-21)
changeset 58747c680f181b32e
parent 58746 68c2cbe2fd3a
child 58748 8f92f17d8781
tuned rendering;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 13:21:59 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 13:56:42 2014 +0200
     1.3 @@ -63,11 +63,11 @@
     1.4    /* overall document structure */
     1.5  
     1.6    sealed abstract class Document { def length: Int }
     1.7 -  case class Document_Block(val name: String, val body: List[Document]) extends Document
     1.8 +  case class Document_Block(name: String, text: String, body: List[Document]) extends Document
     1.9    {
    1.10      val length: Int = (0 /: body)(_ + _.length)
    1.11    }
    1.12 -  case class Document_Atom(val command: Command) extends Document
    1.13 +  case class Document_Atom(command: Command) extends Document
    1.14    {
    1.15      def length: Int = command.length
    1.16    }
    1.17 @@ -301,14 +301,14 @@
    1.18      def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
    1.19        new mutable.ListBuffer[Outer_Syntax.Document]
    1.20  
    1.21 -    var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
    1.22 -      List((0, "", buffer()))
    1.23 +    var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
    1.24 +      List((0, Command.empty, buffer()))
    1.25  
    1.26      @tailrec def close(level: Int => Boolean)
    1.27      {
    1.28        stack match {
    1.29 -        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
    1.30 -          body2 += Outer_Syntax.Document_Block(name, body.toList)
    1.31 +        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    1.32 +          body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
    1.33            stack = stack.tail
    1.34            close(level)
    1.35          case _ =>
    1.36 @@ -326,7 +326,7 @@
    1.37        heading_level(command) match {
    1.38          case Some(i) =>
    1.39            close(_ > i)
    1.40 -          stack = (i + 1, command.source, buffer()) :: stack
    1.41 +          stack = (i + 1, command, buffer()) :: stack
    1.42          case None =>
    1.43        }
    1.44        stack.head._3 += Outer_Syntax.Document_Atom(command)
     2.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Tue Oct 21 13:21:59 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Tue Oct 21 13:56:42 2014 +0200
     2.3 @@ -231,9 +231,8 @@
     2.4    {
     2.5      override def supportsCompletion = false
     2.6  
     2.7 -    private class Asset(
     2.8 -        label: String, label_html: String, start: Text.Offset, stop: Text.Offset, source: String)
     2.9 -      extends Isabelle_Sidekick.Asset(label, start, stop) {
    2.10 +    private class Asset(label: String, label_html: String, range: Text.Range, source: String)
    2.11 +      extends Isabelle_Sidekick.Asset(label, range) {
    2.12          override def getShortString: String = label_html
    2.13          override def getLongString: String = source
    2.14        }
    2.15 @@ -252,7 +251,8 @@
    2.16              val label = kind + (if (name == "") "" else " " + name)
    2.17              val label_html =
    2.18                "<html><b>" + kind + "</b>" + (if (name == "") "" else " " + name) + "</html>"
    2.19 -            val asset = new Asset(label, label_html, offset, offset + source.size, source)
    2.20 +            val range = Text.Range(offset, offset + source.size)
    2.21 +            val asset = new Asset(label, label_html, range, source)
    2.22              data.root.add(new DefaultMutableTreeNode(asset))
    2.23            }
    2.24            offset += source.size
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 13:21:59 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 13:56:42 2014 +0200
     3.3 @@ -30,15 +30,17 @@
     3.4      data
     3.5    }
     3.6  
     3.7 -  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
     3.8 +  class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
     3.9    {
    3.10 -    protected var _name = name
    3.11 -    protected var _start = int_to_pos(start)
    3.12 -    protected var _end = int_to_pos(end)
    3.13 +    protected var _name = text
    3.14 +    protected var _start = int_to_pos(range.start)
    3.15 +    protected var _end = int_to_pos(range.stop)
    3.16      override def getIcon: Icon = null
    3.17      override def getShortString: String =
    3.18        "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
    3.19 -      HTML.encode(_name) + "</span></html>"
    3.20 +      (if (keyword != "" && _name.startsWith(keyword))
    3.21 +        "<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
    3.22 +       else HTML.encode(_name)) + "</span></html>"
    3.23      override def getLongString: String = _name
    3.24      override def getName: String = _name
    3.25      override def setName(name: String) = _name = name
    3.26 @@ -49,6 +51,8 @@
    3.27      override def toString: String = _name
    3.28    }
    3.29  
    3.30 +  class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
    3.31 +
    3.32    def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
    3.33      swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    3.34    {
    3.35 @@ -108,10 +112,11 @@
    3.36      {
    3.37        (offset /: documents) { case (i, document) =>
    3.38          document match {
    3.39 -          case Outer_Syntax.Document_Block(name, body) =>
    3.40 +          case Outer_Syntax.Document_Block(name, text, body) =>
    3.41 +            val range = Text.Range(i, i + document.length)
    3.42              val node =
    3.43                new DefaultMutableTreeNode(
    3.44 -                new Isabelle_Sidekick.Asset(Library.first_line(name), i, i + document.length))
    3.45 +                new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
    3.46              parent.add(node)
    3.47              make_tree(node, i, body)
    3.48            case _ =>
    3.49 @@ -170,7 +175,7 @@
    3.50                      .mkString
    3.51  
    3.52                  new DefaultMutableTreeNode(
    3.53 -                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
    3.54 +                  new Isabelle_Sidekick.Asset(command.toString, range) {
    3.55                      override def getShortString: String = content
    3.56                      override def getLongString: String = info_text
    3.57                      override def toString: String = quote(content) + " " + range.toString
    3.58 @@ -190,7 +195,7 @@
    3.59    private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
    3.60  
    3.61    private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
    3.62 -    new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
    3.63 +    new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
    3.64  
    3.65    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    3.66    {