src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Fri, 23 Dec 2016 17:04:29 +0100
changeset 64665 00aa710ff7f0
parent 64664 951507563033
child 64667 cdb0d559a24b
permissions -rw-r--r--
tuned;
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
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   161
  def goto_file(focus: Boolean, view: View, name: String): Unit =
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   162
    goto_file(focus, view, Line.Node_Position(name))
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   163
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   164
  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   165
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57611
diff changeset
   166
    GUI_Thread.require {}
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   167
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   168
    push_position(view)
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 56373
diff changeset
   169
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   170
    val name = pos.name
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   171
    val line = pos.line
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   172
    val column = pos.column
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   173
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   174
    JEdit_Lib.jedit_buffer(name) match {
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   175
      case Some(buffer) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   176
        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   177
        val text_area = view.getTextArea
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   178
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   179
        try {
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   180
          val line_start = text_area.getBuffer.getLineStartOffset(line)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   181
          text_area.moveCaretPosition(line_start)
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   182
          if (column > 0) text_area.moveCaretPosition(line_start + column)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   183
        }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   184
        catch {
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   185
          case _: ArrayIndexOutOfBoundsException =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   186
          case _: IllegalArgumentException =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   187
        }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   188
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   189
      case None if (new JFile(name)).isDirectory =>
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   190
        VFSBrowser.browseDirectory(view, name)
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   191
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   192
      case None =>
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   193
        val args =
54706
d3c656f0b7ab browse directory hyperlink as well;
wenzelm
parents: 54702
diff changeset
   194
          if (line <= 0) Array(name)
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   195
          else if (column <= 0) Array(name, "+line:" + (line + 1))
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   196
          else Array(name, "+line:" + (line + 1) + "," + (column + 1))
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   197
        jEdit.openFiles(view, null, args)
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   198
    }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   199
  }
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   200
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   201
  def goto_doc(view: View, path: Path)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   202
  {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   203
    if (path.is_file)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   204
      goto_file(true, view, File.platform_path(path))
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   205
    else {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   206
      Standard_Thread.fork("documentation") {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   207
        try { Doc.view(path) }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   208
        catch {
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   209
          case exn: Throwable =>
62062
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   210
            GUI_Thread.later {
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   211
              GUI.error_dialog(view,
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   212
                "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
   213
            }
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   214
        }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   215
      }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   216
    }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   217
  }
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   218
55877
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   219
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   220
  /* hyperlinks */
65c9968286d5 tuned signature;
wenzelm
parents: 55876
diff changeset
   221
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   222
  def hyperlink_doc(name: String): Option[Hyperlink] =
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   223
    Doc.contents().collectFirst({
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   224
      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
   225
      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
   226
        new Hyperlink {
64663
wenzelm
parents: 64662
diff changeset
   227
          override val external = !path.is_file
61660
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   228
          def follow(view: View): Unit = goto_doc(view, path)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   229
          override def toString: String = "doc " + quote(name)
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   230
        })
78b371644654 added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents: 61557
diff changeset
   231
56461
wenzelm
parents: 56458
diff changeset
   232
  def hyperlink_url(name: String): Hyperlink =
wenzelm
parents: 56458
diff changeset
   233
    new Hyperlink {
64663
wenzelm
parents: 64662
diff changeset
   234
      override val external = true
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   235
      def follow(view: View): Unit =
61557
f6387515f951 prefer ad-hoc non-worker threads;
wenzelm
parents: 61544
diff changeset
   236
        Standard_Thread.fork("hyperlink_url") {
62248
dca0bac351b2 allow single quote within URL;
wenzelm
parents: 62062
diff changeset
   237
          try { Isabelle_System.open(Url.escape(name)) }
56461
wenzelm
parents: 56458
diff changeset
   238
          catch {
wenzelm
parents: 56458
diff changeset
   239
            case exn: Throwable =>
62062
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   240
              GUI_Thread.later {
ee610059b0e9 fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents: 61728
diff changeset
   241
                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
   242
              }
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   243
          }
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
   244
        }
56461
wenzelm
parents: 56458
diff changeset
   245
      override def toString: String = "URL " + quote(name)
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
   246
    }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   247
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   248
  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
   249
    new Hyperlink {
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   250
      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
   251
      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
   252
    }
30b75b7958d6 citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents: 57878
diff changeset
   253
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   254
  def hyperlink_file(focus: Boolean, name: String): Hyperlink =
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   255
    hyperlink_file(focus, Line.Node_Position(name))
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   256
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   257
  def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
56461
wenzelm
parents: 56458
diff changeset
   258
    new Hyperlink {
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   259
      def follow(view: View): Unit = goto_file(focus, view, pos)
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   260
      override def toString: String = "file " + quote(pos.name)
56461
wenzelm
parents: 56458
diff changeset
   261
    }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   262
64653
89c5bb2a2128 tuned -- use zero-based Line.Position;
wenzelm
parents: 64613
diff changeset
   263
  def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
55878
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   264
    : Option[Hyperlink] =
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   265
  {
64657
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   266
    for (name <- PIDE.resources.source_file(source_name)) yield {
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   267
      JEdit_Lib.jedit_buffer(name) match {
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   268
        case Some(buffer) if offset > 0 =>
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   269
          val pos =
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   270
            JEdit_Lib.buffer_lock(buffer) {
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   271
              (Line.Position.zero /:
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   272
                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   273
                  zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   274
            }
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   275
          hyperlink_file(focus, Line.Node_Position(name, pos))
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   276
        case _ =>
6209e0f7a4e8 clarified modules;
wenzelm
parents: 64653
diff changeset
   277
          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
55878
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   278
      }
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   279
    }
6d092a5166f1 more precise navigation within open files;
wenzelm
parents: 55877
diff changeset
   280
  }
55876
142139457653 tuned signature;
wenzelm
parents: 55822
diff changeset
   281
56461
wenzelm
parents: 56458
diff changeset
   282
  override def hyperlink_command(
64664
wenzelm
parents: 64663
diff changeset
   283
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   284
      : Option[Hyperlink] =
56461
wenzelm
parents: 56458
diff changeset
   285
  {
wenzelm
parents: 56458
diff changeset
   286
    if (snapshot.is_outdated) None
64665
wenzelm
parents: 64664
diff changeset
   287
    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
56461
wenzelm
parents: 56458
diff changeset
   288
  }
wenzelm
parents: 56458
diff changeset
   289
61011
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   290
  def is_hyperlink_position(snapshot: Document.Snapshot,
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   291
    text_offset: Text.Offset, pos: Position.T): Boolean =
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   292
  {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   293
    pos match {
64662
wenzelm
parents: 64657
diff changeset
   294
      case Position.Item_Id(id, offset) if offset > 0 =>
64665
wenzelm
parents: 64664
diff changeset
   295
        snapshot.find_command(id) match {
61011
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   296
          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   297
            node.command_start(command) match {
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   298
              case Some(start) => text_offset == start + command.chunk.decode(offset)
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   299
              case None => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   300
            }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   301
          case _ => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   302
        }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   303
      case _ => false
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   304
    }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   305
  }
018b0c996b54 more explicit debugger caret rendering;
wenzelm
parents: 60988
diff changeset
   306
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   307
  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   308
      : Option[Hyperlink] =
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   309
    pos match {
64662
wenzelm
parents: 64657
diff changeset
   310
      case Position.Item_File(name, line, offset) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   311
        hyperlink_source_file(focus, name, line, offset)
64662
wenzelm
parents: 64657
diff changeset
   312
      case Position.Item_Id(id, offset) =>
64664
wenzelm
parents: 64663
diff changeset
   313
        hyperlink_command(focus, snapshot, id, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   314
      case _ => None
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   315
    }
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   316
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   317
  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   318
      : Option[Hyperlink] =
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   319
    pos match {
64662
wenzelm
parents: 64657
diff changeset
   320
      case Position.Item_Def_File(name, line, offset) =>
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 60874
diff changeset
   321
        hyperlink_source_file(focus, name, line, offset)
64662
wenzelm
parents: 64657
diff changeset
   322
      case Position.Item_Def_Id(id, offset) =>
64664
wenzelm
parents: 64663
diff changeset
   323
        hyperlink_command(focus, snapshot, id, offset)
60874
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   324
      case _ => None
7865e03a7fc1 tuned signature;
wenzelm
parents: 59319
diff changeset
   325
    }
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
   326
}