--- a/Admin/makedist Wed Dec 09 12:03:27 2009 +0100
+++ b/Admin/makedist Wed Dec 09 12:26:42 2009 +0100
@@ -148,8 +148,6 @@
cp doc/isabelle*.eps lib/logo
-rm Isabelle Isabelle.exe
-
if [ -z "$RELEASE" ]; then
{
--- a/src/Pure/General/swing_thread.scala Wed Dec 09 12:03:27 2009 +0100
+++ b/src/Pure/General/swing_thread.scala Wed Dec 09 12:26:42 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 })
--- a/src/Pure/System/isabelle_system.scala Wed Dec 09 12:03:27 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Dec 09 12:26:42 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")
}
}