author | wenzelm |
Mon, 12 Aug 2013 11:39:29 +0200 | |
changeset 52971 | 31926d2c04ee |
child 52974 | 908e8a36e975 |
permissions | -rw-r--r-- |
/* Title: Pure/PIDE/editor.scala Author: Makarius General editor operations. */ package isabelle abstract class Editor[Context] { def session: Session def current_context: Context def current_node(context: Context): Option[Document.Node.Name] def current_snapshot(context: Context): Option[Document.Snapshot] def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] }