isabelle: src/Pure/PIDE/editor.scala@40630fec3b5d (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
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73340 diff changeset	10	abstract class Editor[Context] {
66082 2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	11	/* session */
2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	12
52971 31926d2c04ee tuned signature -- more abstract PIDE editor operations; wenzelm parents: diff changeset	13	def session: Session
66084 7f8eeff20f7a tuned signature; wenzelm parents: 66082 diff changeset	14	def flush(): Unit
54461 6c360a6ade0e centralized management of pending buffer edits; wenzelm parents: 53844 diff changeset	15	def invoke(): Unit
66101 0f0f294e314f maintain overlays within main state of document models; wenzelm parents: 66094 diff changeset	16
0f0f294e314f maintain overlays within main state of document models; wenzelm parents: 66094 diff changeset	17
0f0f294e314f maintain overlays within main state of document models; wenzelm parents: 66094 diff changeset	18	/* current situation */
0f0f294e314f maintain overlays within main state of document models; wenzelm parents: 66094 diff changeset	19
52971 31926d2c04ee tuned signature -- more abstract PIDE editor operations; wenzelm parents: diff changeset	20	def current_node(context: Context): Option[Document.Node.Name]
52978 37fbb3fde380 prefer PIDE editor operations; wenzelm parents: 52977 diff changeset	21	def current_node_snapshot(context: Context): Option[Document.Snapshot]
52974 908e8a36e975 tuned signature; wenzelm parents: 52971 diff changeset	22	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	23	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	24
66082 2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	25
2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	26	/* overlays */
2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	27
66101 0f0f294e314f maintain overlays within main state of document models; wenzelm parents: 66094 diff changeset	28	def node_overlays(name: Document.Node.Name): Document.Node.Overlays
73340 0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 66101 diff changeset	29	def insert_overlay(command: Command, fn: String, args: List[String]): Unit
0ffcad1f6130 tuned --- fewer warnings; wenzelm parents: 66101 diff changeset	30	def remove_overlay(command: Command, fn: String, args: List[String]): Unit
66082 2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	31
2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	32
2d12a730a380 clarified modules; wenzelm parents: 64867 diff changeset	33	/* hyperlinks */
52980 28f59ca8ce78 manage hyperlinks via PIDE editor interface; wenzelm parents: 52978 diff changeset	34
75393 87ebf5a50283 clarified formatting, for the sake of scala3; wenzelm parents: 73340 diff changeset	35	abstract class Hyperlink {
64663 4c9fb4d4bca3 tuned; wenzelm parents: 64524 diff changeset	36	def external: Boolean = false
56494 1b74abf064e1 avoid confusion about pointless cursor movement with external links; wenzelm parents: 55884 diff changeset	37	def follow(context: Context): Unit
1b74abf064e1 avoid confusion about pointless cursor movement with external links; wenzelm parents: 55884 diff changeset	38	}
66084 7f8eeff20f7a tuned signature; wenzelm parents: 66082 diff changeset	39
52980 28f59ca8ce78 manage hyperlinks via PIDE editor interface; wenzelm parents: 52978 diff changeset	40	def hyperlink_command(
64664 951507563033 tuned; wenzelm parents: 64663 diff changeset	41	focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
60893 3c8b9b4b577c support hyperlinks with optional focus change; wenzelm parents: 56494 diff changeset	42	: Option[Hyperlink]
66094 24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	43
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	44
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	45	/* dispatcher thread */
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	46
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	47	def assert_dispatcher[A](body: => A): A
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	48	def require_dispatcher[A](body: => A): A
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	49	def send_dispatcher(body: => Unit): Unit
24658c9d7c78 more general dispatcher operations; wenzelm parents: 66084 diff changeset	50	def send_wait_dispatcher(body: => Unit): Unit
52971 31926d2c04ee tuned signature -- more abstract PIDE editor operations; wenzelm parents: diff changeset	51	}

author	wenzelm
	Sat, 09 Apr 2022 15:28:55 +0200
changeset 75436	40630fec3b5d
parent 75393	87ebf5a50283
child 76609	cc9ddf373bd2
permissions	-rw-r--r--