isabelle: src/Pure/PIDE/editor.scala@52125652e82a (annotated)

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

author	wenzelm
	Fri, 25 Apr 2014 12:51:08 +0200
changeset 56715	52125652e82a
parent 56494	1b74abf064e1
child 60893	3c8b9b4b577c
permissions	-rw-r--r--