# HG changeset patch
# User wenzelm
# Date 1273661400 -7200
# Node ID 0cdfce0bf956c26751c091592cc945134ea1c1bd
# Parent  fc8a6b5f9b0b64940ef35af60f519cbc4eae5b15
clarified Pretty.font_metrics;

diff -r fc8a6b5f9b0b -r 0cdfce0bf956 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed May 12 11:31:05 2010 +0200
+++ b/src/Pure/General/pretty.scala	Wed May 12 12:50:00 2010 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.awt.FontMetrics
+
+
 object Pretty
 {
   /* markup trees with physical blocks and breaks */
@@ -64,6 +67,13 @@
   private val margin_default = 76
   private def metric_default(s: String) = s.length.toDouble
 
+  def font_metric(metrics: FontMetrics): String => Double =
+    if (metrics == null) ((s: String) => s.length.toDouble)
+    else {
+      val unit = metrics.charWidth(Symbol.spc).toDouble
+      ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
+    }
+
   def formatted(input: List[XML.Tree], margin: Int = margin_default,
     metric: String => Double = metric_default): List[XML.Tree] =
   {
diff -r fc8a6b5f9b0b -r 0cdfce0bf956 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Wed May 12 11:31:05 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Wed May 12 12:50:00 2010 +0200
@@ -85,10 +85,10 @@
 """
   }
 
-  def font_metrics(font_size: Int): FontMetrics =
+  private def font_metrics(font_size: Int): FontMetrics =
     Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
 
-  def panel_width(font_size: Int): Int =
+  private def panel_width(font_size: Int): Int =
     Swing_Thread.now {
       (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
     }
@@ -129,10 +129,6 @@
     var current_font_size = 16
     var current_font_metrics: FontMetrics = null
 
-    def metric(s: String): Double =
-      if (current_font_metrics == null) s.length.toDouble
-      else current_font_metrics.stringWidth(s).toDouble / current_font_metrics.charWidth(Symbol.spc)
-
     loop {
       react {
         case Init(font_size) =>
@@ -150,7 +146,8 @@
           val doc = doc2
           val html_body =
             divs.flatMap(div =>
-              Pretty.formatted(List(div), panel_width(current_font_size), metric)
+              Pretty.formatted(List(div), panel_width(current_font_size),
+                  Pretty.font_metric(current_font_metrics))
                 .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
           val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
           doc.removeChild(doc.getLastChild())