isabelle: src/Tools/jEdit/src-base/plugin.scala@c87ca43ebd3b (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
73110 c87ca43ebd3b avoid rescaled fonts, e.g. dockable buttons on Windows L&F after opening a new view; wenzelm parents: 73076 diff changeset	22	GUI.use_isabelle_fonts()
c87ca43ebd3b avoid rescaled fonts, e.g. dockable buttons on Windows L&F after opening a new view; wenzelm parents: 73076 diff changeset	23
66593 d389714a8aaa clarified startup sequence; wenzelm parents: 66590 diff changeset	24	Debug.DISABLE_SEARCH_DIALOG_POOL = true
d389714a8aaa clarified startup sequence; wenzelm parents: 66590 diff changeset	25
66602 180b2e72601f more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; wenzelm parents: 66593 diff changeset	26	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	27	}
66590 8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	28
8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	29	override def stop()
8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	30	{
66602 180b2e72601f more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache; wenzelm parents: 66593 diff changeset	31	Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
66590 8e1aac4eed11 more robust; wenzelm parents: 66555 diff changeset	32	}
66603 f6a1274be674 tuned signature -- avoid warning during jEdit startup; wenzelm parents: 66602 diff changeset	33
f6a1274be674 tuned signature -- avoid warning during jEdit startup; wenzelm parents: 66602 diff changeset	34	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	35	}

author	wenzelm
	Fri, 08 Jan 2021 22:30:32 +0100
changeset 73110	c87ca43ebd3b
parent 73076	d44552bf310f
child 73340	0ffcad1f6130
permissions	-rw-r--r--