src/Pure/PIDE/editor.scala
author wenzelm
Wed, 09 Apr 2014 13:32:34 +0200
changeset 56494 1b74abf064e1
parent 55884 f2c0eaedd579
child 60893 3c8b9b4b577c
permissions -rw-r--r--
avoid confusion about pointless cursor movement with external links;
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
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52971
diff changeset
    13
  def flush(): Unit
54461
6c360a6ade0e centralized management of pending buffer edits;
wenzelm
parents: 53844
diff changeset
    14
  def invoke(): Unit
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    15
  def current_context: Context
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    16
  def current_node(context: Context): Option[Document.Node.Name]
52978
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52977
diff changeset
    17
  def current_node_snapshot(context: Context): Option[Document.Snapshot]
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52971
diff changeset
    18
  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
    19
  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
    20
15254e32d299 central management of Document.Overlays, independent of Document_Model;
wenzelm
parents: 52974
diff changeset
    21
  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
    22
  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
    23
  def remove_overlay(command: Command, fn: String, args: List[String]): Unit
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    24
56494
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    25
  abstract class Hyperlink {
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    26
    def external: Boolean
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    27
    def follow(context: Context): Unit
1b74abf064e1 avoid confusion about pointless cursor movement with external links;
wenzelm
parents: 55884
diff changeset
    28
  }
52980
28f59ca8ce78 manage hyperlinks via PIDE editor interface;
wenzelm
parents: 52978
diff changeset
    29
  def hyperlink_command(
55884
f2c0eaedd579 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents: 55876
diff changeset
    30
    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    31
}
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff changeset
    32