Sidekick block asset: show first line only;
authorwenzelm
Wed, 10 Nov 2010 20:43:22 +0100
changeset 407448a57ff2c2600
parent 40743 576b88b1dce9
child 40745 515eab39b6c2
Sidekick block asset: show first line only;
src/Pure/library.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/library.scala	Wed Nov 10 20:21:55 2010 +0100
     1.2 +++ b/src/Pure/library.scala	Wed Nov 10 20:43:22 2010 +0100
     1.3 @@ -82,6 +82,13 @@
     1.4        }
     1.5    }
     1.6  
     1.7 +  def first_line(source: CharSequence): String =
     1.8 +  {
     1.9 +    val lines = chunks(source)
    1.10 +    if (lines.hasNext) lines.next.toString
    1.11 +    else ""
    1.12 +  }
    1.13 +
    1.14  
    1.15    /* simple dialogs */
    1.16  
     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 20:21:55 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 20:43:22 2010 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4          case Structure.Block(name, body) =>
     2.5            val node =
     2.6              new DefaultMutableTreeNode(
     2.7 -              new Isabelle_Sidekick.Asset(name, offset, offset + entry.length))
     2.8 +              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
     2.9            (offset /: body)((i, e) =>
    2.10              {
    2.11                make_tree(i, e) foreach (nd => node.add(nd))