--- a/src/Tools/jEdit/lib/Tools/jedit Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Aug 24 16:45:55 2012 +0200
@@ -12,8 +12,8 @@
"src/document_model.scala"
"src/document_view.scala"
"src/html_panel.scala"
+ "src/hyperlink.scala"
"src/isabelle_encoding.scala"
- "src/isabelle_hyperlinks.scala"
"src/isabelle_options.scala"
"src/isabelle_rendering.scala"
"src/isabelle_sidekick.scala"
@@ -167,7 +167,6 @@
JEDIT_JARS=(
"$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
- "$ISABELLE_JEDIT_BUILD_HOME/contrib/Hyperlinks.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
--- a/src/Tools/jEdit/src/Isabelle.props Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Aug 24 16:45:55 2012 +0200
@@ -18,7 +18,6 @@
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.4.1
plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.8
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 0.8
-plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.jedit.hyperlinks.HyperlinksPlugin 1.0.1
#options
plugin.isabelle.jedit.Plugin.option-pane=isabelle
@@ -78,5 +77,3 @@
mode.ml.sidekick.parser=isabelle
sidekick.parser.isabelle.label=Isabelle
-#Hyperlinks
-mode.isabelle.hyperlink.source=isabelle
--- a/src/Tools/jEdit/src/document_view.scala Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Aug 24 16:45:55 2012 +0200
@@ -17,7 +17,7 @@
import java.lang.System
import java.text.BreakIterator
import java.awt.{Color, Graphics2D, Point}
-import java.awt.event.{MouseMotionAdapter, MouseEvent,
+import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
import javax.swing.event.{CaretListener, CaretEvent}
@@ -181,22 +181,28 @@
}
- /* subexpression highlighting */
+ /* subexpression highlighting and hyperlinks */
@volatile private var _highlight_range: Option[Text.Info[Color]] = None
def highlight_range(): Option[Text.Info[Color]] = _highlight_range
+ @volatile private var _hyperlink_range: Option[Text.Info[Hyperlink]] = None
+ def hyperlink_range(): Option[Text.Info[Hyperlink]] = _hyperlink_range
+
private var control: Boolean = false
private def exit_control()
{
exit_popup()
_highlight_range = None
+ _hyperlink_range = None
}
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) {
- _highlight_range = None // FIXME exit_control !?
+ // FIXME exit_control !?
+ _highlight_range = None
+ _hyperlink_range = None
}
}
@@ -205,6 +211,15 @@
override def windowDeactivated(e: WindowEvent) { exit_control() }
}
+ private val mouse_listener = new MouseAdapter {
+ override def mouseClicked(e: MouseEvent) {
+ hyperlink_range match {
+ case Some(Text.Info(range, link)) => link.follow(text_area.getView)
+ case None =>
+ }
+ }
+ }
+
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
Swing_Thread.assert()
@@ -220,14 +235,22 @@
if (control) init_popup(snapshot, x, y)
- for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
- _highlight_range =
- if (control) {
- val offset = text_area.xyToOffset(x, y)
- Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
- }
- else None
- for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
+ def update_range[A](
+ rendering: (Document.Snapshot, Text.Range) => Option[Text.Info[A]],
+ info: Option[Text.Info[A]]): Option[Text.Info[A]] =
+ {
+ for (Text.Info(range, _) <- info) invalidate_range(range)
+ val new_info =
+ if (control) {
+ val offset = text_area.xyToOffset(x, y)
+ rendering(snapshot, Text.Range(offset, offset + 1))
+ }
+ else None
+ for (Text.Info(range, _) <- info) invalidate_range(range)
+ new_info
+ }
+ _highlight_range = update_range(Isabelle_Rendering.subexp, _highlight_range)
+ _hyperlink_range = update_range(Isabelle_Rendering.hyperlink, _hyperlink_range)
}
}
}
@@ -395,6 +418,7 @@
text_area.getGutter.addExtension(gutter_painter)
text_area.addFocusListener(focus_listener)
text_area.getView.addWindowListener(window_listener)
+ painter.addMouseListener(mouse_listener)
painter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
@@ -410,6 +434,7 @@
text_area.removeFocusListener(focus_listener)
text_area.getView.removeWindowListener(window_listener)
painter.removeMouseMotionListener(mouse_motion_listener)
+ painter.removeMouseListener(mouse_listener)
text_area.removeCaretListener(caret_listener); delay_caret_update(false)
text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
text_area.getGutter.removeExtension(gutter_painter)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/hyperlink.scala Fri Aug 24 16:45:55 2012 +0200
@@ -0,0 +1,63 @@
+/* Title: Tools/jEdit/src/hyperlink.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+Hyperlinks within jEdit buffers for PIDE proof documents.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.io.{File => JFile}
+
+import org.gjt.sp.jedit.{View, jEdit}
+import org.gjt.sp.jedit.textarea.JEditTextArea
+
+
+object Hyperlink
+{
+ def apply(file: JFile, line: Int, column: Int): Hyperlink =
+ File_Link(file, line, column)
+}
+
+abstract class Hyperlink
+{
+ def follow(view: View): Unit
+}
+
+private case class File_Link(file: JFile, line: Int, column: Int) extends Hyperlink
+{
+ override def follow(view: View)
+ {
+ Swing_Thread.require()
+
+ val full_name = file.getCanonicalPath
+ val base_name = file.getName
+
+ Isabelle.jedit_buffer(full_name) match {
+ case Some(buffer) =>
+ view.setBuffer(buffer)
+ val text_area = view.getTextArea
+
+ try {
+ val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
+ text_area.moveCaretPosition(line_start)
+ if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
+ }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+
+ case None =>
+ val args =
+ if (line <= 0) Array(base_name)
+ else if (column <= 0) Array(base_name, "+line:" + line.toInt)
+ else Array(base_name, "+line:" + line.toInt + "," + column.toInt)
+ jEdit.openFiles(view, file.getParent, args)
+ }
+ }
+}
+
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Fri Aug 24 16:43:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-/* Title: Tools/jEdit/src/isabelle_hyperlinks.scala
- Author: Fabian Immler, TU Munich
-
-Hyperlink setup for Isabelle proof documents.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.io.{File => JFile}
-
-import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
-
-import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
-
-
-private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)
- extends AbstractHyperlink(start, end, line, "")
-{
- override def click(view: View)
- {
- val text_area = view.getTextArea
- if (Isabelle.buffer_name(view.getBuffer) == name)
- text_area.moveCaretPosition(offset)
- else
- Isabelle.jedit_buffer(name) match {
- case Some(buffer) =>
- view.setBuffer(buffer)
- text_area.moveCaretPosition(offset)
- case None =>
- }
- }
-}
-
-class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
- extends AbstractHyperlink(start, end, line, "")
-{
- override def click(view: View) = {
- Isabelle_System.source_file(Path.explode(def_file)) match {
- case None =>
- Library.error_dialog(view, "File not found",
- Library.scrollable_text("Could not find source file " + def_file))
- case Some(file) =>
- jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
- }
- }
-}
-
-class Isabelle_Hyperlinks extends HyperlinkSource
-{
- def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
- {
- Swing_Thread.assert()
- Isabelle.buffer_lock(buffer) {
- Document_Model(buffer) match {
- case Some(model) =>
- val snapshot = model.snapshot()
- val markup =
- snapshot.select_markup[Hyperlink](
- Text.Range(buffer_offset, buffer_offset + 1),
- Some(Set(Isabelle_Markup.ENTITY)),
- {
- // FIXME Isabelle_Rendering.hyperlink
- case Text.Info(info_range,
- XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
- if (props.find(
- { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
- case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
- case _ => false }).isEmpty) =>
- 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), 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)) =>
- snapshot.state.find_command(snapshot.version, def_id) match {
- case Some((def_node, def_cmd)) =>
- def_node.command_start(def_cmd) match {
- case Some(def_cmd_start) =>
- new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
- def_cmd_start + def_cmd.decode(def_offset))
- case None => null
- }
- case None => null
- }
- case _ => null
- }
- case _ => null
- }
- })
- markup match {
- case Text.Info(_, link) #:: _ => link
- case _ => null
- }
- case None => null
- }
- }
- }
-}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Aug 24 16:45:55 2012 +0200
@@ -11,6 +11,7 @@
import java.awt.Color
import javax.swing.Icon
+import java.io.{File => JFile}
import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
@@ -42,6 +43,7 @@
val quoted_color = new Color(139, 139, 139, 25)
val subexp_color = new Color(80, 80, 80, 50)
+ val hyperlink_color = Color.BLACK
val keyword1_color = get_color("#006699")
val keyword2_color = get_color("#009966")
@@ -98,12 +100,67 @@
{
snapshot.select_markup(range, Some(subexp_include),
{
- case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- Text.Info(snapshot.convert(range), subexp_color)
+ case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ Text.Info(snapshot.convert(info_range), subexp_color)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
}
+ private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
+
+ def hyperlink(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Hyperlink]] =
+ {
+ snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
+ {
+ case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
+ if Path.is_ok(name) =>
+ val file = Path.explode(name).file
+ Text.Info(snapshot.convert(info_range), Hyperlink(file, 0, 0)) :: links
+
+ case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
+ if (props.find(
+ { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
+ case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
+ case _ => false }).isEmpty) =>
+
+ props match {
+ case Position.Line_File(line, name) if Path.is_ok(name) =>
+ Isabelle_System.source_file(Path.explode(name)) match {
+ case Some(file) =>
+ Text.Info(snapshot.convert(info_range), Hyperlink(file, line, 0)) :: links
+ case None => links
+ }
+
+ case Position.Id_Offset(def_id, def_offset) if !snapshot.is_outdated =>
+ snapshot.state.find_command(snapshot.version, def_id) match {
+ case Some((def_node, def_cmd)) =>
+ val file = new JFile(def_cmd.node_name.node)
+
+ // FIXME move!?
+ val sources =
+ def_node.commands.iterator.takeWhile(_ != def_cmd).map(_.source) ++
+ Iterator.single(def_cmd.source(Text.Range(0, def_offset)))
+ var line = 1
+ var column = 1
+ for (source <- sources) {
+ val newlines = (0 /: source.iterator) { // FIXME Symbol.iterator!?
+ case (n, c) => if (c == '\n') n + 1 else n }
+ if (newlines > 0) {
+ line += newlines
+ column = source.lastIndexOf('\n') + 2
+ }
+ }
+ Text.Info(snapshot.convert(info_range), Hyperlink(file, line, column)) :: links
+
+ case None => links
+ }
+
+ case _ => links
+ }
+ }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
+ }
+
+
private def tooltip_text(msg: XML.Tree): String =
Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
--- a/src/Tools/jEdit/src/services.xml Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/src/services.xml Fri Aug 24 16:45:55 2012 +0200
@@ -17,9 +17,6 @@
<SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Raw();
</SERVICE>
- <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
- new isabelle.jedit.Isabelle_Hyperlinks();
- </SERVICE>
<SERVICE CLASS="console.Shell" NAME="Scala">
new isabelle.jedit.Scala_Console();
</SERVICE>
--- a/src/Tools/jEdit/src/text_area_painter.scala Fri Aug 24 16:43:37 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Aug 24 16:45:55 2012 +0200
@@ -341,6 +341,16 @@
gfx.setColor(color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
+
+ // hyperlink range -- potentially from other snapshot
+ for {
+ info <- doc_view.hyperlink_range()
+ Text.Info(range, _) <- info.try_restrict(line_range)
+ r <- gfx_range(range)
+ } {
+ gfx.setColor(Isabelle_Rendering.hyperlink_color)
+ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+ }
}
}
}