# HG changeset patch # User wenzelm # Date 1334775972 -7200 # Node ID 3982d300475819c68db3e224f52eb179f1726c8d # Parent bd6c65d46b851456cdd0159dce49d80ce550fddc# Parent 9980c0c094b8449d2323526cfb95cd4169111f7b merged diff -r bd6c65d46b85 -r 3982d3004758 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Wed Apr 18 21:06:12 2012 +0200 @@ -155,15 +155,13 @@ } def swing_tree(parent: DefaultMutableTreeNode) - (swing_node: Text.Markup => DefaultMutableTreeNode) + (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode) { for ((_, entry) <- branches) { var current = parent - for (info <- entry.markup) { - val node = swing_node(Text.Info(entry.range, info)) - current.add(node) - current = node - } + val node = swing_node(Text.Info(entry.range, entry.markup)) + current.add(node) + current = node entry.subtree.swing_tree(current)(swing_node) } } diff -r bd6c65d46b85 -r 3982d3004758 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 18 21:06:12 2012 +0200 @@ -154,6 +154,15 @@ case _ => false } + object Sendback + { + def unapply(msg: Any): Option[XML.Body] = + msg match { + case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body) + case _ => None + } + } + /* reported positions */ diff -r bd6c65d46b85 -r 3982d3004758 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Pure/PIDE/text.scala Wed Apr 18 21:06:12 2012 +0200 @@ -41,6 +41,8 @@ override def toString = "[" + start.toString + ":" + stop.toString + "]" + def length: Int = stop - start + def map(f: Offset => Offset): Range = Range(f(start), f(stop)) def +(i: Offset): Range = map(_ + i) def -(i: Offset): Range = map(_ - i) diff -r bd6c65d46b85 -r 3982d3004758 src/Tools/jEdit/etc/isabelle-jedit.css --- a/src/Tools/jEdit/etc/isabelle-jedit.css Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css Wed Apr 18 21:06:12 2012 +0200 @@ -15,5 +15,5 @@ .operator { font-weight: bold; } .command { font-weight: bold; color: #006699; } -.sendback { text-decoration: underline; } -.sendback:hover { background-color: #FFCC66; } +.sendback { background-color: #DCDCDC; } +.sendback:hover { background-color: #9DC75D; } diff -r bd6c65d46b85 -r 3982d3004758 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Apr 18 21:06:12 2012 +0200 @@ -71,8 +71,8 @@ val Text.Range(begin, end) = info_range val line = buffer.getLineOfOffset(begin) (Position.File.unapply(props), Position.Line.unapply(props)) match { - case (Some(def_file), Some(def_line)) => - new External_Hyperlink(begin, end, line, def_file, def_line) + case (Some(def_file), def_line) => + new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1)) case _ if !snapshot.is_outdated => (props, props) match { case (Position.Id(def_id), Position.Offset(def_offset)) => diff -r bd6c65d46b85 -r 3982d3004758 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Apr 18 21:06:12 2012 +0200 @@ -147,24 +147,26 @@ def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] = { - def add(prev: Text.Info[List[String]], r: Text.Range, s: String) = - if (prev.range == r) Text.Info(r, s :: prev.info) else Text.Info(r, List(s)) + def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) = + if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p)) val tips = - snapshot.cumulate_markup[Text.Info[List[String]]]( + snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]]( range, Text.Info(range, Nil), Some(tooltip_elements), { case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) => - add(prev, r, kind + " " + quote(name)) + add(prev, r, (true, kind + " " + quote(name))) case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) => - add(prev, r, string_of_typing("::", body)) + add(prev, r, (true, string_of_typing("::", body))) case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) => - add(prev, r, string_of_typing("ML:", body)) + add(prev, r, (false, string_of_typing("ML:", body))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) - if tooltips.isDefinedAt(name) => add (prev, r, tooltips(name)) + if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name))) }).toList.flatMap(_.info.info) - if (tips.isEmpty) None else Some(cat_lines(tips)) + val all_tips = + (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2) + if (all_tips.isEmpty) None else Some(cat_lines(all_tips)) } diff -r bd6c65d46b85 -r 3982d3004758 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 18 21:06:12 2012 +0200 @@ -155,15 +155,12 @@ val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range() if !stopped) { snapshot.state.command_state(snapshot.version, command).markup - .swing_tree(root)((info: Text.Markup) => + .swing_tree(root)((info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start val content = command.source(info.range).replace('\n', ' ') val info_text = - info.info match { - case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString - case x => x.toString - } + Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString new DefaultMutableTreeNode( new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { diff -r bd6c65d46b85 -r 3982d3004758 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Wed Apr 18 20:47:21 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Wed Apr 18 21:06:12 2012 +0200 @@ -28,22 +28,34 @@ private val html_panel = new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) { - override val handler: PartialFunction[HTML_Panel.Event, Unit] = { - case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" => - val text = elem.getFirstChild().getNodeValue() - + override val handler: PartialFunction[HTML_Panel.Event, Unit] = + { + case HTML_Panel.Mouse_Click(elem, event) + if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined => + val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get Document_View(view.getTextArea) match { case Some(doc_view) => - val cmd = current_command.get - val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get - val buffer = view.getBuffer - buffer.beginCompoundEdit() - buffer.remove(start_ofs, cmd.length) - buffer.insert(start_ofs, text) - buffer.endCompoundEdit() + doc_view.robust_body() { + current_command match { + case Some(cmd) => + val model = doc_view.model + val buffer = model.buffer + val snapshot = model.snapshot() + snapshot.node.command_start(cmd) match { + case Some(start) if !snapshot.is_outdated => + val text = Pretty.string_of(sendback) + buffer.beginCompoundEdit() + buffer.remove(start, cmd.proper_range.length) + buffer.insert(start, text) + buffer.endCompoundEdit() + case _ => + } + case None => + } + } case None => } - } + } } set_content(html_panel)