equal
deleted
inserted
replaced
1 /* Title: Pure/GUI/jfx_thread.scala |
1 /* Title: Pure/GUI/jfx_thread.scala |
|
2 Module: PIDE-GUI |
2 Author: Makarius |
3 Author: Makarius |
3 |
4 |
4 Evaluation within the Java FX application thread. |
5 Evaluation within the Java FX application thread. |
5 */ |
6 */ |
6 |
7 |