# HG changeset patch # User wenzelm # Date 1380048088 -7200 # Node ID e8430d668f44c8693536e39461fc52185842b41c # Parent c7707223d782945a4cfa00b1aaa92cc60da3d985 more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material); diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/color_value.scala --- a/src/Pure/GUI/color_value.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/color_value.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/color_value.scala + Module: PIDE-GUI Author: Makarius Cached color values. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/gui.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/gui.scala + Module: PIDE-GUI Author: Makarius Basic GUI tools (for AWT/Swing). diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/html5_panel.scala --- a/src/Pure/GUI/html5_panel.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/html5_panel.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/html5_panel.scala + Module: PIDE-GUI Author: Makarius HTML5 panel based on Java FX WebView. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/jfx_thread.scala --- a/src/Pure/GUI/jfx_thread.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/jfx_thread.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/jfx_thread.scala + Module: PIDE-GUI Author: Makarius Evaluation within the Java FX application thread. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/popup.scala --- a/src/Pure/GUI/popup.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/popup.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/popup.scala + Module: PIDE-GUI Author: Makarius Popup within layered pane. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/swing_thread.scala --- a/src/Pure/GUI/swing_thread.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/swing_thread.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/swing_thread.scala + Module: PIDE-GUI Author: Makarius Evaluation within the AWT/Swing thread. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/system_dialog.scala --- a/src/Pure/GUI/system_dialog.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/system_dialog.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/system_dialog.scala + Module: PIDE-GUI Author: Makarius Dialog for system processes, with optional output window. diff -r c7707223d782 -r e8430d668f44 src/Pure/GUI/wrap_panel.scala --- a/src/Pure/GUI/wrap_panel.scala Tue Sep 24 20:24:14 2013 +0200 +++ b/src/Pure/GUI/wrap_panel.scala Tue Sep 24 20:41:28 2013 +0200 @@ -1,4 +1,5 @@ /* Title: Pure/GUI/wrap_panel.scala + Module: PIDE-GUI Author: Makarius Panel with improved FlowLayout for wrapping of components over