--- a/src/Pure/PIDE/markup_tree.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Wed Apr 18 21:28:49 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)
}
}
--- a/src/Pure/PIDE/protocol.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Apr 18 21:28:49 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 */
--- a/src/Pure/PIDE/text.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Pure/PIDE/text.scala Wed Apr 18 21:28:49 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)
--- a/src/Tools/jEdit/etc/isabelle-jedit.css Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css Wed Apr 18 21:28:49 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; }
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Apr 18 21:28:49 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)) =>
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Apr 18 21:28:49 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))
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 18 21:28:49 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) {
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Apr 18 21:11:50 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Apr 18 21:28:49 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)