src/Pure/PIDE/editor.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 64867 e7220f4de11f
child 66082 2d12a730a380
permissions -rw-r--r--
clarified modules;
     1 /*  Title:      Pure/PIDE/editor.scala
     2     Author:     Makarius
     3 
     4 General editor operations.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 abstract class Editor[Context]
    11 {
    12   def session: Session
    13   def flush(hidden: Boolean = false, purge: Boolean = false): Unit
    14   def invoke(): Unit
    15   def invoke_generated(): Unit
    16   def current_context: Context
    17   def current_node(context: Context): Option[Document.Node.Name]
    18   def current_node_snapshot(context: Context): Option[Document.Snapshot]
    19   def node_snapshot(name: Document.Node.Name): Document.Snapshot
    20   def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
    21 
    22   def node_overlays(name: Document.Node.Name): Document.Node.Overlays
    23   def insert_overlay(command: Command, fn: String, args: List[String]): Unit
    24   def remove_overlay(command: Command, fn: String, args: List[String]): Unit
    25 
    26   abstract class Hyperlink {
    27     def external: Boolean = false
    28     def follow(context: Context): Unit
    29   }
    30   def hyperlink_command(
    31     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
    32       : Option[Hyperlink]
    33 }
    34