tuned;
authorwenzelm
Sat, 01 Mar 2014 19:43:35 +0100
changeset 55826 e56a52dd770a
parent 55825 694833e3e4a0
child 55827 8a881f83e206
tuned;
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/pretty_text_area.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
--- 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