# HG changeset patch # User wenzelm # Date 1260356031 -3600 # Node ID 8ab37779a8e6f2672e8c2f817a561fa69e6c37a7 # Parent 08d34921b7dd049b6c6e5d293a25661adb2620f3# Parent ce25a3b37111cb86ed33e8a67e5d2cd3848b78ef merged diff -r 08d34921b7dd -r 8ab37779a8e6 src/Pure/General/swing_thread.scala --- a/src/Pure/General/swing_thread.scala Tue Dec 08 23:05:23 2009 +0100 +++ b/src/Pure/General/swing_thread.scala Wed Dec 09 11:53:51 2009 +0100 @@ -10,6 +10,8 @@ import javax.swing.{SwingUtilities, Timer} import java.awt.event.{ActionListener, ActionEvent} +import scala.actors.{Future, Futures} + object Swing_Thread { @@ -21,13 +23,17 @@ /* main dispatch queue */ - def now[A](body: => A): A = { + def now[A](body: => A): A = + { var result: Option[A] = None if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) result.get } + def future[A](body: => A): Future[A] = + Futures.future(now(body)) + def later(body: => Unit) { if (SwingUtilities.isEventDispatchThread()) body else SwingUtilities.invokeLater(new Runnable { def run = body }) diff -r 08d34921b7dd -r 8ab37779a8e6 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue Dec 08 23:05:23 2009 +0100 +++ b/src/Pure/System/isabelle_system.scala Wed Dec 09 11:53:51 2009 +0100 @@ -341,11 +341,11 @@ private def create_font(name: String) = Font.createFont(Font.TRUETYPE_FONT, platform_file(name)) - def register_fonts(): Boolean = - { + def register_fonts() { val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() val ok1 = ge.registerFont(create_font("~~/lib/fonts/IsabelleText.ttf")) val ok2 = ge.registerFont(create_font("~~/lib/fonts/IsabelleTextBold.ttf")) - ok1 && ok2 + if (!(ok1 && ok2) && !ge.getAvailableFontFamilyNames.contains(font_family)) + error("Font family " + font_family + " unavailable") } }