isabelle: src/Tools/jEdit/src-base/plugin.scala@180b2e72601f (annotated)

66457 9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	1	/* Title: Tools/jEdit/src-base/plugin.scala
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	2	Author: Makarius
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	3
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	4	Isabelle base environment for jEdit.
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	5	*/
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	6
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	7	package isabelle.jedit_base
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	8
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	9
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	10	import isabelle._
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	11
66593 d389714a8aaa clarified startup sequence; wenzelm parents: 66590 diff changeset	12	import org.gjt.sp.jedit.{Debug, EBPlugin}
66555 39257f39c7da more robust: fall-back for SyntaxUtilities.StyleExtender when Isabelle plugin is unloaded; wenzelm parents: 66457 diff changeset	13	import org.gjt.sp.util.SyntaxUtilities
66457 9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	14
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	15
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	16	class Plugin extends EBPlugin
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	17	{
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	18	override def start()
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	19	{
9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	20	Isabelle_System.init()
66555 39257f39c7da more robust: fall-back for SyntaxUtilities.StyleExtender when Isabelle plugin is unloaded; wenzelm parents: 66457 diff changeset	21
66593 d389714a8aaa clarified startup sequence; wenzelm parents: 66590 diff changeset	22	Debug.DISABLE_SEARCH_DIALOG_POOL = true
d389714a8aaa clarified startup sequence; wenzelm parents: 66590 diff changeset	23
66602 180b2e72601f more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; wenzelm parents: 66593 diff changeset	24	Syntax_Style.dummy_style_extender()
66457 9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	25	}
66590 8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	26
8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	27	override def stop()
8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	28	{
66602 180b2e72601f more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; wenzelm parents: 66593 diff changeset	29	Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
66590 8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	30	}
66457 9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	31	}

author	wenzelm
	Mon, 04 Sep 2017 15:25:25 +0200
changeset 66602	180b2e72601f
parent 66593	d389714a8aaa
child 66603	f6a1274be674
permissions	-rw-r--r--