src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Thu, 24 Nov 2016 15:21:54 +0100
changeset 64524 e6a3c55b929b
parent 64521 1aef5a0e18d7
child 64612 08e4b1aeac50
permissions -rw-r--r--
explicit option editor_generated_input_delay, which is more aggressive by default;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_editor.scala
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     3
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     4
PIDE editor operations for jEdit.
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     5
*/
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     6
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     8
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
     9
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    10
import isabelle._
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    11
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    12
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
    13
import java.io.{File => JFile}
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
    14
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
    15
import org.gjt.sp.jedit.{jEdit, View, Buffer}
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
    16
import org.gjt.sp.jedit.browser.VFSBrowser
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    17
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    18
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    19
class JEdit_Editor extends Editor[View]
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    20
{
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    21
  /* session */
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    22
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    23
  override def session: Session = PIDE.session
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    24
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    25
  // owned by GUI thread
57611
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    26
  private var removed_nodes = Set.empty[Document.Node.Name]
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    27
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    28
  def remove_node(name: Document.Node.Name): Unit =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    29
    GUI_Thread.require { removed_nodes += name }
57611
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    30
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61660
diff changeset
    31
  override def flush(hidden: Boolean = false)
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    32
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    33
    GUI_Thread.require {}
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    34
55783
da0513d95155 more formal Document.Blobs;
wenzelm
parents: 55781
diff changeset
    35
    val doc_blobs = PIDE.document_blobs()
57611
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    36
    val models = PIDE.document_models()
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    37
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    38
    val removed = removed_nodes; removed_nodes = Set.empty
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    39
    val removed_perspective =
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    40
      (removed -- models.iterator.map(_.node_name)).toList.map(
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57612
diff changeset
    41
        name => (name, Document.Node.no_perspective_text))
57611
b6256ea3b7c5 proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents: 56770
diff changeset
    42
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 61660
diff changeset
    43
    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
61544
19d84de5f534 redundant;
wenzelm
parents: 61011
diff changeset
    44
    session.update(doc_blobs, edits)
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    45
  }
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    46
64524
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    47
  private val delay1_flush =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    48
    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
54461
6c360a6ade0e centralized management of pending buffer edits;
wenzelm
parents: 54325
diff changeset
    49
64524
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    50
  private val delay2_flush =
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    51
    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
64521
1aef5a0e18d7 delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
wenzelm
parents: 62248
diff changeset
    52
64524
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    53
  def invoke(): Unit = delay1_flush.invoke()
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    54
  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
54461
6c360a6ade0e centralized management of pending buffer edits;
wenzelm
parents: 54325
diff changeset
    55
60933
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    56
  def stable_tip_version(): Option[Document.Version] =
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    57
    GUI_Thread.require {
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    58
      if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    59
        session.current_state().stable_tip_version
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    60
      else None
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    61
    }
6d03e05ef041 more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents: 60893
diff changeset
    62
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    63
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    64
  /* current situation */
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    65
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    66
  override def current_context: View =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    67
    GUI_Thread.require { jEdit.getActiveView() }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    68
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    69
  override def current_node(view: View): Option[Document.Node.Name] =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    70
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    71
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    72
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    73
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    74
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    75
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    76
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    77
    GUI_Thread.require {}
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    78
56457
eea4bbe15745 tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents: 56413
diff changeset
    79
    JEdit_Lib.jedit_buffer(name) match {
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    80
      case Some(buffer) =>
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    81
        PIDE.document_model(buffer) match {
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    82
          case Some(model) => model.snapshot
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    83
          case None => session.snapshot(name)
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    84
        }
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    85
      case None => session.snapshot(name)
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    86
    }
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    87
  }
908e8a36e975 tuned signature;
wenzelm
parents: 52973
diff changeset
    88
53844
71f103629327 skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents: 52980
diff changeset
    89
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    90
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
    91
    GUI_Thread.require {}
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    92
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
    93
    val text_area = view.getTextArea
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
    94
    val buffer = view.getBuffer
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
    95
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
    96
    PIDE.document_view(text_area) match {
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 54706
diff changeset
    97
      case Some(doc_view) if doc_view.model.is_theory =>
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
    98
        val node = snapshot.version.nodes(doc_view.model.node_name)
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
    99
        val caret = snapshot.revert(text_area.getCaretPosition)
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   100
        if (caret < buffer.getLength) {
56373
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56314
diff changeset
   101
          val caret_command_iterator = node.command_iterator(caret)
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56314
diff changeset
   102
          if (caret_command_iterator.hasNext) {
0605d90be6fc tuned signature -- more explicit iterator terminology;
wenzelm
parents: 56314
diff changeset
   103
            val (cmd0, _) = caret_command_iterator.next
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
   104
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
53844
71f103629327 skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents: 52980
diff changeset
   105
          }
54325
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
   106
          else None
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
   107
        }
2c4155003352 clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents: 53845
diff changeset
   108
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
55432
9c53198dbb1c maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents: 54706
diff changeset
   109
      case _ =>
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   110
        PIDE.document_model(buffer) match {
54531
8330faaeebd5 restrict node_required status and Theories panel to actual theories;
wenzelm
parents: 54528
diff changeset
   111
          case Some(model) if !model.is_theory =>
56314
9a513737a0b2 tuned signature;
wenzelm
parents: 55884
diff changeset
   112
            snapshot.version.nodes.load_commands(model.node_name) match {
54528
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   113
              case cmd :: _ => Some(cmd)
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   114
              case Nil => None
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   115
            }
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   116
          case _ => None
842adea880a4 refer to thy_load command of auxiliary file;
wenzelm
parents: 54522
diff changeset
   117
        }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
   118
    }
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
   119
  }
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   120
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   121
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   122
  /* overlays */
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   123
57873
ea94d2aa62be clarified synchronized scope;
wenzelm
parents: 57615
diff changeset
   124
  private val overlays = Synchronized(Document.Overlays.empty)
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   125
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   126
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
57873
ea94d2aa62be clarified synchronized scope;
wenzelm
parents: 57615
diff changeset
   127
    overlays.value(name)
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   128
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   129
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
57873
ea94d2aa62be clarified synchronized scope;
wenzelm
parents: 57615
diff changeset
   130
    overlays.change(_.insert(command, fn, args))
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
   131
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   132
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
57873
ea94d2aa62be clarified synchronized scope;
wenzelm
parents: 57615
diff changeset
   133
    overlays.change(_.remove(command, fn, args))
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   134
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   135
55877
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   136
  /* navigation */
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   137
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   138
  def push_position(view: View)
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   139
  {
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   140
    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   141
    if (navigator != null) {
59080
611914621edb added Untyped.method convenience (for *this* class only);
wenzelm
parents: 58545
diff changeset
   142
      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   143
      catch { case _: NoSuchMethodException => }
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   144
    }
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   145
  }
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   146
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   147
  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   148
  {
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   149
    GUI_Thread.require {}
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   150
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   151
    push_position(view)
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   152
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   153
    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   154
    try { view.getTextArea.moveCaretPosition(offset) }
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   155
    catch {
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   156
      case _: ArrayIndexOutOfBoundsException =>
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   157
      case _: IllegalArgumentException =>
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   158
    }
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   159
  }
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   160
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   161
  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   162
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
   163
    GUI_Thread.require {}
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   164
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   165
    push_position(view)
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   166
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   167
    JEdit_Lib.jedit_buffer(name) match {
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   168
      case Some(buffer) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   169
        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   170
        val text_area = view.getTextArea
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   171
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   172
        try {
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   173
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   174
          text_area.moveCaretPosition(line_start)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   175
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   176
        }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   177
        catch {
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   178
          case _: ArrayIndexOutOfBoundsException =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   179
          case _: IllegalArgumentException =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   180
        }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   181
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   182
      case None if (new JFile(name)).isDirectory =>
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   183
        VFSBrowser.browseDirectory(view, name)
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   184
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   185
      case None =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   186
        val args =
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   187
          if (line <= 0) Array(name)
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   188
          else if (column <= 0) Array(name, "+line:" + line.toInt)
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   189
          else Array(name, "+line:" + line.toInt + "," + column.toInt)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   190
        jEdit.openFiles(view, null, args)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   191
    }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   192
  }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   193
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   194
  def goto_doc(view: View, path: Path)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   195
  {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   196
    if (path.is_file)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   197
      goto_file(true, view, File.platform_path(path))
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   198
    else {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   199
      Standard_Thread.fork("documentation") {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   200
        try { Doc.view(path) }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   201
        catch {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   202
          case exn: Throwable =>
62062
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   203
            GUI_Thread.later {
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   204
              GUI.error_dialog(view,
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   205
                "Documentation error", GUI.scrollable_text(Exn.message(exn)))
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   206
            }
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   207
        }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   208
      }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   209
    }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   210
  }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   211
55877
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   212
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   213
  /* hyperlinks */
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   214
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   215
  def hyperlink_doc(name: String): Option[Hyperlink] =
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   216
    Doc.contents().collectFirst({
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   217
      case doc: Doc.Text_File if doc.name == name => doc.path
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   218
      case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   219
        new Hyperlink {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   220
          val external = !path.is_file
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   221
          def follow(view: View): Unit = goto_doc(view, path)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   222
          override def toString: String = "doc " + quote(name)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   223
        })
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   224
56461
wenzelm
parents: 56458
diff changeset
   225
  def hyperlink_url(name: String): Hyperlink =
wenzelm
parents: 56458
diff changeset
   226
    new Hyperlink {
56494
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 56462
diff changeset
   227
      val external = true
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   228
      def follow(view: View): Unit =
61557
f6387515f951 prefer ad-hoc non-worker threads;
wenzelm
parents: 61544
diff changeset
   229
        Standard_Thread.fork("hyperlink_url") {
62248
dca0bac351b2 allow single quote within URL;
wenzelm
parents: 62062
diff changeset
   230
          try { Isabelle_System.open(Url.escape(name)) }
56461
wenzelm
parents: 56458
diff changeset
   231
          catch {
wenzelm
parents: 56458
diff changeset
   232
            case exn: Throwable =>
62062
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   233
              GUI_Thread.later {
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   234
                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   235
              }
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   236
          }
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   237
        }
56461
wenzelm
parents: 56458
diff changeset
   238
      override def toString: String = "URL " + quote(name)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   239
    }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   240
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   241
  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   242
    new Hyperlink {
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   243
      val external = false
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   244
      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
58545
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   245
      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   246
    }
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   247
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   248
  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
56461
wenzelm
parents: 56458
diff changeset
   249
    new Hyperlink {
56494
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 56462
diff changeset
   250
      val external = false
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   251
      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
56461
wenzelm
parents: 56458
diff changeset
   252
      override def toString: String = "file " + quote(name)
wenzelm
parents: 56458
diff changeset
   253
    }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   254
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   255
  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
55878
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   256
    : Option[Hyperlink] =
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   257
  {
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   258
    val opt_name =
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   259
      if (Path.is_wellformed(source_name)) {
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   260
        if (Path.is_valid(source_name)) {
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   261
          val path = Path.explode(source_name)
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 60933
diff changeset
   262
          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   263
        }
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   264
        else None
55878
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   265
      }
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   266
      else Some(source_name)
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   267
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   268
    opt_name match {
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   269
      case Some(name) =>
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   270
        JEdit_Lib.jedit_buffer(name) match {
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   271
          case Some(buffer) if offset > 0 =>
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   272
            val (line, column) =
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   273
              JEdit_Lib.buffer_lock(buffer) {
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   274
                ((1, 1) /:
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   275
                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   276
                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   277
                      Symbol.advance_line_column)
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   278
              }
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   279
            Some(hyperlink_file(focus, name, line, column))
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   280
          case _ => Some(hyperlink_file(focus, name, line))
56458
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   281
        }
a8d960baa5c2 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents: 56457
diff changeset
   282
      case None => None
55878
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   283
    }
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   284
  }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   285
56461
wenzelm
parents: 56458
diff changeset
   286
  override def hyperlink_command(
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   287
    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   288
      : Option[Hyperlink] =
56461
wenzelm
parents: 56458
diff changeset
   289
  {
wenzelm
parents: 56458
diff changeset
   290
    if (snapshot.is_outdated) None
wenzelm
parents: 56458
diff changeset
   291
    else {
wenzelm
parents: 56458
diff changeset
   292
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm
parents: 56458
diff changeset
   293
        case None => None
wenzelm
parents: 56458
diff changeset
   294
        case Some((node, _)) =>
wenzelm
parents: 56458
diff changeset
   295
          val file_name = command.node_name.node
wenzelm
parents: 56458
diff changeset
   296
          val sources_iterator =
wenzelm
parents: 56458
diff changeset
   297
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm
parents: 56458
diff changeset
   298
              (if (offset == 0) Iterator.empty
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 56461
diff changeset
   299
               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
56461
wenzelm
parents: 56458
diff changeset
   300
          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   301
          Some(hyperlink_file(focus, file_name, line, column))
56461
wenzelm
parents: 56458
diff changeset
   302
      }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   303
    }
56461
wenzelm
parents: 56458
diff changeset
   304
  }
wenzelm
parents: 56458
diff changeset
   305
wenzelm
parents: 56458
diff changeset
   306
  def hyperlink_command_id(
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   307
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   308
      : Option[Hyperlink] =
56461
wenzelm
parents: 56458
diff changeset
   309
  {
wenzelm
parents: 56458
diff changeset
   310
    snapshot.state.find_command(snapshot.version, id) match {
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   311
      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
56461
wenzelm
parents: 56458
diff changeset
   312
      case None => None
wenzelm
parents: 56458
diff changeset
   313
    }
wenzelm
parents: 56458
diff changeset
   314
  }
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   315
61011
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   316
  def is_hyperlink_position(snapshot: Document.Snapshot,
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   317
    text_offset: Text.Offset, pos: Position.T): Boolean =
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   318
  {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   319
    pos match {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   320
      case Position.Id_Offset0(id, offset) if offset > 0 =>
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   321
        snapshot.state.find_command(snapshot.version, id) match {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   322
          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   323
            node.command_start(command) match {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   324
              case Some(start) => text_offset == start + command.chunk.decode(offset)
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   325
              case None => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   326
            }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   327
          case _ => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   328
        }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   329
      case _ => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   330
    }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   331
  }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   332
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   333
  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   334
      : Option[Hyperlink] =
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   335
    pos match {
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   336
      case Position.Line_File(line, name) =>
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   337
        val offset = Position.Offset.unapply(pos) getOrElse 0
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   338
        hyperlink_source_file(focus, name, line, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   339
      case Position.Id_Offset0(id, offset) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   340
        hyperlink_command_id(focus, snapshot, id, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   341
      case _ => None
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   342
    }
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   343
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   344
  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   345
      : Option[Hyperlink] =
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   346
    pos match {
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   347
      case Position.Def_Line_File(line, name) =>
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   348
        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   349
        hyperlink_source_file(focus, name, line, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   350
      case Position.Def_Id_Offset0(id, offset) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   351
        hyperlink_command_id(focus, snapshot, id, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   352
      case _ => None
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   353
    }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
   354
}