src/Tools/jEdit/src/isabelle_hyperlinks.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 43606 e1a09c2a6248
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 42327
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_hyperlinks.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Fabian Immler, TU Munich
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
Hyperlink setup for Isabelle proof documents.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
*/
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
     6
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
     7
package isabelle.jedit
34569
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
     8
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
     9
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    11
34569
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    12
import java.io.File
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    13
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34788
diff changeset
    14
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    15
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34788
diff changeset
    16
import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    17
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34582
diff changeset
    18
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    19
private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
34569
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    20
  extends AbstractHyperlink(start, end, line, "")
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    21
{
34582
5d5d253c7c29 superficial tuning;
wenzelm
parents: 34573
diff changeset
    22
  override def click(view: View) {
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    23
    view.getTextArea.moveCaretPosition(def_offset)
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    24
  }
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    25
}
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    26
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    27
class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
34569
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    28
  extends AbstractHyperlink(start, end, line, "")
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    29
{
34602
782b1948aca9 ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents: 34588
diff changeset
    30
  override def click(view: View) = {
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    31
    Isabelle.system.source_file(def_file) match {
38853
f593754b0772 External_Hyperlink: proper error dialog;
wenzelm
parents: 38845
diff changeset
    32
      case None =>
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    33
        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
34602
782b1948aca9 ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents: 34588
diff changeset
    34
      case Some(file) =>
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    35
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
34573
daa397b6401c changed handling of subdirectories
immler@in.tum.de
parents: 34569
diff changeset
    36
    }
34602
782b1948aca9 ExternalHyperlink.click: use IsabelleSystem.source_file provided in http://isabelle.in.tum.de/repos/isabelle/rev/dde1b4d1c95b
wenzelm
parents: 34588
diff changeset
    37
  }
34569
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    38
}
15abc5f5f40a implemented links to other files
immler@in.tum.de
parents: 34568
diff changeset
    39
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    40
class Isabelle_Hyperlinks extends HyperlinkSource
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    41
{
38575
80d962964216 Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm
parents: 38427
diff changeset
    42
  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36990
diff changeset
    43
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38153
diff changeset
    44
    Swing_Thread.assert()
38843
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    45
    Isabelle.buffer_lock(buffer) {
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    46
      Document_Model(buffer) match {
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    47
        case Some(model) =>
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    48
          val snapshot = model.snapshot()
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    49
          val markup =
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    50
            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
38843
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    51
              // FIXME Isar_Document.Hyperlink extractor
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    52
              case Text.Info(info_range,
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    53
                  XML.Elem(Markup(Markup.ENTITY, props), _))
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    54
                if (props.find(
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    55
                  { case (Markup.KIND, Markup.ML_OPEN) => true
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    56
                    case (Markup.KIND, Markup.ML_STRUCT) => true
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    57
                    case _ => false }).isEmpty) =>
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    58
                val Text.Range(begin, end) = info_range
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    59
                val line = buffer.getLineOfOffset(begin)
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    60
                (Position.File.unapply(props), Position.Line.unapply(props)) match {
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    61
                  case (Some(def_file), Some(def_line)) =>
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    62
                    new External_Hyperlink(begin, end, line, def_file, def_line)
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    63
                  case _ =>
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    64
                    (props, props) match {
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    65
                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    66
                        snapshot.lookup_command(def_id) match {
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    67
                          case Some(def_cmd) =>
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    68
                            snapshot.node.command_start(def_cmd) match {
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    69
                              case Some(def_cmd_start) =>
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    70
                                new Internal_Hyperlink(begin, end, line,
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 39177
diff changeset
    71
                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    72
                              case None => null
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    73
                            }
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    74
                          case None => null
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    75
                        }
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    76
                      case _ => null
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    77
                    }
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
    78
                }
39177
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38853
diff changeset
    79
            }
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38853
diff changeset
    80
          markup match {
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38853
diff changeset
    81
            case Text.Info(_, Some(link)) #:: _ => link
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38853
diff changeset
    82
            case _ => null
0468964aec11 simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
wenzelm
parents: 38853
diff changeset
    83
          }
38843
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    84
        case None => null
d95522496593 more careful locking of jEdit buffer;
wenzelm
parents: 38722
diff changeset
    85
      }
34568
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    86
    }
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    87
  }
b517d0607297 implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
diff changeset
    88
}