tuned;
authorwenzelm
Sat Mar 01 19:43:35 2014 +0100 (2014-03-01)
changeset 55826e56a52dd770a
parent 55825 694833e3e4a0
child 55827 8a881f83e206
tuned;
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/pretty_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:39:27 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:43:35 2014 +0100
     1.3 @@ -17,9 +17,6 @@
     1.4  
     1.5  object Font_Info
     1.6  {
     1.7 -  val dummy: Font_Info = Font_Info("Dialog", 12.0f)
     1.8 -
     1.9 -
    1.10    /* size range */
    1.11  
    1.12    val min_size = 5
     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 19:39:27 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 01 19:43:35 2014 +0100
     2.3 @@ -61,7 +61,7 @@
     2.4  
     2.5    Swing_Thread.require()
     2.6  
     2.7 -  private var current_font_info: Font_Info = Font_Info.dummy
     2.8 +  private var current_font_info: Font_Info = Font_Info.main()
     2.9    private var current_body: XML.Body = Nil
    2.10    private var current_base_snapshot = Document.Snapshot.init
    2.11    private var current_base_results = Command.Results.empty