| author | haftmann |
| Thu, 24 Jul 2025 17:46:29 +0200 | |
| changeset 82902 | 99a720d3ed8f |
| parent 73994 | fbb30dac95a2 |
| permissions | -rw-r--r-- |
|
73994
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/jedit_main/services.scala |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
3 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle/jEdit services. |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
6 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit_main |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
8 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
9 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
10 |
class Fold_Handler extends isabelle.jedit.Fold_Handling.Fold_Handler |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
11 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
12 |
class Context_Menu extends isabelle.jedit.Context_Menu |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
13 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
14 |
class Isabelle_Export_VFS extends isabelle.jedit.Isabelle_Export.VFS |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
15 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
16 |
class Isabelle_Session_VFS extends isabelle.jedit.Isabelle_Session.VFS |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
17 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
18 |
class Active_Misc_Handler extends isabelle.jedit.Active.Misc_Handler |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
19 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
20 |
class Graphview_Dockable_Handler extends isabelle.jedit.Graphview_Dockable.Handler |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
21 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
22 |
class Status_Widget_Java_Factory extends isabelle.jedit.Status_Widget.Java_Factory |
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
23 |
|
|
fbb30dac95a2
clarified startup: implicitly enforce activation of isabelle.jedit_main.Plugin;
wenzelm
parents:
diff
changeset
|
24 |
class Status_Widget_ML_Factory extends isabelle.jedit.Status_Widget.ML_Factory |