1.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 20:47:21 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 21:06:12 2012 +0200
     1.3 @@ -155,15 +155,13 @@
     1.4    }
     1.5  
     1.6    def swing_tree(parent: DefaultMutableTreeNode)
     1.7 -    (swing_node: Text.Markup => DefaultMutableTreeNode)
     1.8 +    (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
     1.9    {
    1.10      for ((_, entry) <- branches) {
    1.11        var current = parent
    1.12 -      for (info <- entry.markup) {
    1.13 -        val node = swing_node(Text.Info(entry.range, info))
    1.14 -        current.add(node)
    1.15 -        current = node
    1.16 -      }
    1.17 +      val node = swing_node(Text.Info(entry.range, entry.markup))
    1.18 +      current.add(node)
    1.19 +      current = node
    1.20        entry.subtree.swing_tree(current)(swing_node)
    1.21      }
    1.22    }

     2.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 18 20:47:21 2012 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 18 21:06:12 2012 +0200
     2.3 @@ -154,6 +154,15 @@
     2.4        case _ => false
     2.5      }
     2.6  
     2.7 +  object Sendback
     2.8 +  {
     2.9 +    def unapply(msg: Any): Option[XML.Body] =
    2.10 +      msg match {
    2.11 +        case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body)
    2.12 +        case _ => None
    2.13 +      }
    2.14 +  }
    2.15 +
    2.16  
    2.17    /* reported positions */
    2.18  

     3.1 --- a/src/Pure/PIDE/text.scala	Wed Apr 18 20:47:21 2012 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Wed Apr 18 21:06:12 2012 +0200
     3.3 @@ -41,6 +41,8 @@
     3.4  
     3.5      override def toString = "[" + start.toString + ":" + stop.toString + "]"
     3.6  
     3.7 +    def length: Int = stop - start
     3.8 +
     3.9      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
    3.10      def +(i: Offset): Range = map(_ + i)
    3.11      def -(i: Offset): Range = map(_ - i)

     4.1 --- a/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Apr 18 20:47:21 2012 +0200
     4.2 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Apr 18 21:06:12 2012 +0200
     4.3 @@ -15,5 +15,5 @@
     4.4  .operator { font-weight: bold; }
     4.5  .command { font-weight: bold; color: #006699; }
     4.6  
     4.7 -.sendback { text-decoration: underline; }
     4.8 -.sendback:hover { background-color: #FFCC66; }
     4.9 +.sendback { background-color: #DCDCDC; }
    4.10 +.sendback:hover { background-color: #9DC75D; }

     5.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 20:47:21 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Apr 18 21:06:12 2012 +0200
     5.3 @@ -71,8 +71,8 @@
     5.4                    val Text.Range(begin, end) = info_range
     5.5                    val line = buffer.getLineOfOffset(begin)
     5.6                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
     5.7 -                    case (Some(def_file), Some(def_line)) =>
     5.8 -                      new External_Hyperlink(begin, end, line, def_file, def_line)
     5.9 +                    case (Some(def_file), def_line) =>
    5.10 +                      new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1))
    5.11                      case _ if !snapshot.is_outdated =>
    5.12                        (props, props) match {
    5.13                          case (Position.Id(def_id), Position.Offset(def_offset)) =>

     6.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Apr 18 20:47:21 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Apr 18 21:06:12 2012 +0200
     6.3 @@ -147,24 +147,26 @@
     6.4  
     6.5    def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
     6.6    {
     6.7 -    def add(prev: Text.Info[List[String]], r: Text.Range, s: String) =
     6.8 -      if (prev.range == r) Text.Info(r, s :: prev.info) else Text.Info(r, List(s))
     6.9 +    def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
    6.10 +      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
    6.11  
    6.12      val tips =
    6.13 -      snapshot.cumulate_markup[Text.Info[List[String]]](
    6.14 +      snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
    6.15          range, Text.Info(range, Nil), Some(tooltip_elements),
    6.16          {
    6.17            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
    6.18 -            add(prev, r, kind + " " + quote(name))
    6.19 +            add(prev, r, (true, kind + " " + quote(name)))
    6.20            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
    6.21 -            add(prev, r, string_of_typing("::", body))
    6.22 +            add(prev, r, (true, string_of_typing("::", body)))
    6.23            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
    6.24 -            add(prev, r, string_of_typing("ML:", body))
    6.25 +            add(prev, r, (false, string_of_typing("ML:", body)))
    6.26            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
    6.27 -          if tooltips.isDefinedAt(name) => add (prev, r, tooltips(name))
    6.28 +          if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
    6.29          }).toList.flatMap(_.info.info)
    6.30  
    6.31 -    if (tips.isEmpty) None else Some(cat_lines(tips))
    6.32 +    val all_tips =
    6.33 +      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    6.34 +    if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
    6.35    }
    6.36  
    6.37  

     7.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 20:47:21 2012 +0200
     7.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 21:06:12 2012 +0200
     7.3 @@ -155,15 +155,12 @@
     7.4      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     7.5      for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     7.6        snapshot.state.command_state(snapshot.version, command).markup
     7.7 -        .swing_tree(root)((info: Text.Markup) =>
     7.8 +        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
     7.9            {
    7.10              val range = info.range + command_start
    7.11              val content = command.source(info.range).replace('\n', ' ')
    7.12              val info_text =
    7.13 -              info.info match {
    7.14 -                case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString
    7.15 -                case x => x.toString
    7.16 -              }
    7.17 +              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
    7.18  
    7.19              new DefaultMutableTreeNode(
    7.20                new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {

     8.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 20:47:21 2012 +0200
     8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 21:06:12 2012 +0200
     8.3 @@ -28,22 +28,34 @@
     8.4    private val html_panel =
     8.5      new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
     8.6    {
     8.7 -    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
     8.8 -      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
     8.9 -        val text = elem.getFirstChild().getNodeValue()
    8.10 -
    8.11 +    override val handler: PartialFunction[HTML_Panel.Event, Unit] =
    8.12 +    {
    8.13 +      case HTML_Panel.Mouse_Click(elem, event)
    8.14 +      if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined =>
    8.15 +        val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
    8.16          Document_View(view.getTextArea) match {
    8.17            case Some(doc_view) =>
    8.18 -            val cmd = current_command.get
    8.19 -            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
    8.20 -            val buffer = view.getBuffer
    8.21 -            buffer.beginCompoundEdit()
    8.22 -            buffer.remove(start_ofs, cmd.length)
    8.23 -            buffer.insert(start_ofs, text)
    8.24 -            buffer.endCompoundEdit()
    8.25 +            doc_view.robust_body() {
    8.26 +              current_command match {
    8.27 +                case Some(cmd) =>
    8.28 +                  val model = doc_view.model
    8.29 +                  val buffer = model.buffer
    8.30 +                  val snapshot = model.snapshot()
    8.31 +                  snapshot.node.command_start(cmd) match {
    8.32 +                    case Some(start) if !snapshot.is_outdated =>
    8.33 +                      val text = Pretty.string_of(sendback)
    8.34 +                      buffer.beginCompoundEdit()
    8.35 +                      buffer.remove(start, cmd.proper_range.length)
    8.36 +                      buffer.insert(start, text)
    8.37 +                      buffer.endCompoundEdit()
    8.38 +                    case _ =>
    8.39 +                  }
    8.40 +                case None =>
    8.41 +              }
    8.42 +            }
    8.43            case None =>
    8.44          }
    8.45 -    }       
    8.46 +    }
    8.47    }
    8.48  
    8.49    set_content(html_panel)