isabelle: src/Tools/jEdit/src-base/plugin.scala@39044da8bb5a (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
66603 f6a1274be674 tuned signature -- avoid warning during jEdit startup; wenzelm parents: 66602 diff changeset	12	import org.gjt.sp.jedit.{EBMessage, 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	}
66603 f6a1274be674 tuned signature -- avoid warning during jEdit startup; wenzelm parents: 66602 diff changeset	31
f6a1274be674 tuned signature -- avoid warning during jEdit startup; wenzelm parents: 66602 diff changeset	32	override def handleMessage(message: EBMessage) { }
66457 9098c36abd1a separate base plugin for important services that should be always available, despite startup errors of the main plugin; wenzelm parents: diff changeset	33	}

author	wenzelm
	Sun, 11 Nov 2018 12:13:24 +0100
changeset 69283	39044da8bb5a
parent 66603	f6a1274be674
child 73070	7ef8d77ee761
permissions	-rw-r--r--