author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 66603 | f6a1274be674 |
child 73070 | 7ef8d77ee761 |
permissions | -rw-r--r-- |
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 | 22 |
Debug.DISABLE_SEARCH_DIALOG_POOL = true |
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 | 26 |
|
27 |
override def stop() |
|
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 | 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 |
} |