# HG changeset patch
# User wenzelm
# Date 1393699415 -3600
# Node ID e56a52dd770a52abc6393e2bc2b28d18eace531e
# Parent  694833e3e4a0e7cf9285e6ad41c7611d5c2a9b20
tuned;

diff -r 694833e3e4a0 -r e56a52dd770a src/Tools/jEdit/src/font_info.scala
--- 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
diff -r 694833e3e4a0 -r e56a52dd770a src/Tools/jEdit/src/pretty_text_area.scala
--- 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