--- a/src/Tools/jEdit/src/font_info.scala Sat Mar 01 19:39:27 2014 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Sat Mar 01 19:43:35 2014 +0100
@@ -17,9 +17,6 @@
object Font_Info
{
- val dummy: Font_Info = Font_Info("Dialog", 12.0f)
-
-
/* size range */
val min_size = 5
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 19:39:27 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Mar 01 19:43:35 2014 +0100
@@ -61,7 +61,7 @@
Swing_Thread.require()
- private var current_font_info: Font_Info = Font_Info.dummy
+ private var current_font_info: Font_Info = Font_Info.main()
private var current_body: XML.Body = Nil
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty