1.1 --- a/src/Pure/PIDE/markup_tree.scala Wed Apr 18 21:11:50 2012 +0200
1.2 +++ b/src/Pure/PIDE/markup_tree.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
2.2 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
3.2 +++ b/src/Pure/PIDE/text.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
4.2 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
5.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
6.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
7.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 18 21:28:49 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 21:11:50 2012 +0200
8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala Wed Apr 18 21:28:49 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)