src/Pure/PIDE/editor.scala
author wenzelm
Fri, 23 Dec 2016 15:53:53 +0100
changeset 64663 4c9fb4d4bca3
parent 64524 e6a3c55b929b
child 64664 951507563033
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:      Pure/PIDE/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
General editor operations.
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
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
abstract class Editor[Context]
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
  def session: Session
61728
5f5ff1eab407 double flush to ensure persistent "state" output is reset;
wenzelm
parents: 60893
diff changeset
    13
  def flush(hidden: Boolean = true): Unit
54461
6c360a6ade0e centralized management of pending buffer edits;
wenzelm
parents: 53844
diff changeset
    14
  def invoke(): Unit
64524
e6a3c55b929b explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents: 64521
diff changeset
    15
  def invoke_generated(): Unit
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    16
  def current_context: Context
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    17
  def current_node(context: Context): Option[Document.Node.Name]
52978
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52977
diff changeset
    18
  def current_node_snapshot(context: Context): Option[Document.Snapshot]
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52971
diff changeset
    19
  def node_snapshot(name: Document.Node.Name): Document.Snapshot
53844
71f103629327 skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents: 52980
diff changeset
    20
  def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
52977
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    21
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    22
  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    23
  def insert_overlay(command: Command, fn: String, args: List[String]): Unit
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    24
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    25
56494
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    26
  abstract class Hyperlink {
64663
wenzelm
parents: 64524
diff changeset
    27
    def external: Boolean = false
56494
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    28
    def follow(context: Context): Unit
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    29
  }
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    30
  def hyperlink_command(
60893
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 56494
diff changeset
    31
    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
3c8b9b4b577c support hyperlinks with optional focus change;
wenzelm
parents: 56494
diff changeset
    32
      : Option[Hyperlink]
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    33
}
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    34