# HG changeset patch
# User wenzelm
# Date 1273661492 -7200
# Node ID fa3322113480dba8f23af6ca2c4fe9e676494800
# Parent  691a55e1aeb2695cf0a3357a2cc14d0a5172d824# Parent  0cdfce0bf956c26751c091592cc945134ea1c1bd
merged

diff -r 691a55e1aeb2 -r fa3322113480 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Pure/General/pretty.scala	Wed May 12 12:51:32 2010 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.awt.FontMetrics
+
+
 object Pretty
 {
   /* markup trees with physical blocks and breaks */
@@ -45,32 +48,6 @@
 
   /* formatted output */
 
-  private case class Text(tx: List[XML.Tree] = Nil, val pos: Int = 0, val nl: Int = 0)
-  {
-    def newline: Text = copy(tx = FBreak :: tx, pos = 0, nl = nl + 1)
-    def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + s.length)
-    def blanks(wd: Int): Text = string(Symbol.spaces(wd))
-    def content: List[XML.Tree] = tx.reverse
-  }
-
-  private def breakdist(trees: List[XML.Tree], after: Int): Int =
-    trees match {
-      case Break(_) :: _ => 0
-      case FBreak :: _ => 0
-      case XML.Elem(_, _, body) :: ts =>
-        (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
-      case XML.Text(s) :: ts => s.length + breakdist(ts, after)
-      case Nil => after
-    }
-
-  private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
-    trees match {
-      case Nil => Nil
-      case FBreak :: _ => trees
-      case Break(_) :: ts => FBreak :: ts
-      case t :: ts => t :: forcenext(ts)
-    }
-
   private def standard_format(tree: XML.Tree): List[XML.Tree] =
     tree match {
       case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
@@ -79,14 +56,53 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  private val margin_default = 76
+  case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0)
+  {
+    def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
+    def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
+    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+    def content: List[XML.Tree] = tx.reverse
+  }
 
-  def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
+  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] =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
 
-    def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text =
+    def content_length(tree: XML.Tree): Double =
+      tree match {
+        case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
+        case XML.Text(s) => metric(s)
+      }
+
+    def breakdist(trees: List[XML.Tree], after: Double): Double =
+      trees match {
+        case Break(_) :: _ => 0.0
+        case FBreak :: _ => 0.0
+        case t :: ts => content_length(t) + breakdist(ts, after)
+        case Nil => after
+      }
+
+    def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+      trees match {
+        case Nil => Nil
+        case FBreak :: _ => trees
+        case Break(_) :: ts => FBreak :: ts
+        case t :: ts => t :: forcenext(ts)
+      }
+
+    def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
@@ -103,20 +119,21 @@
         case Break(wd) :: ts =>
           if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
             format(ts, blockin, after, text.blanks(wd))
-          else format(ts, blockin, after, text.newline.blanks(blockin))
-        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
+          else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
+        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
 
         case XML.Elem(name, atts, body) :: ts =>
           val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
           val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
           format(ts1, blockin, after, btext1)
-        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
       }
-    format(input.flatMap(standard_format), 0, 0, Text()).content
+    format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
+  def string_of(input: List[XML.Tree], margin: Int = margin_default,
+      metric: String => Double = metric_default): String =
     formatted(input).iterator.flatMap(XML.content).mkString
 
 
@@ -128,7 +145,7 @@
       tree match {
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
-        case FBreak => List(XML.Text(" "))
+        case FBreak => List(XML.Text(Symbol.space))
         case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
diff -r 691a55e1aeb2 -r fa3322113480 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Pure/General/symbol.scala	Wed May 12 12:51:32 2010 +0200
@@ -15,13 +15,16 @@
 {
   /* spaces */
 
-  private val static_spaces = " " * 4000
+  val spc = ' '
+  val space = " "
+
+  private val static_spaces = space * 4000
 
   def spaces(k: Int): String =
   {
     require(k >= 0)
     if (k < static_spaces.length) static_spaces.substring(0, k)
-    else " " * k
+    else space * k
   }
 
 
@@ -278,7 +281,7 @@
       "\\<^isub>", "\\<^isup>")
 
     private val blanks =
-      Decode_Set(" ", "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+      Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
 
     private val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
diff -r 691a55e1aeb2 -r fa3322113480 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Pure/General/xml.scala	Wed May 12 12:51:32 2010 +0200
@@ -92,12 +92,6 @@
     }
   }
 
-  def content_length(tree: XML.Tree): Int =
-    tree match {
-      case Elem(_, _, body) => (0 /: body)(_ + content_length(_))
-      case Text(s) => s.length
-    }
-
 
   /* cache for partial sharing -- NOT THREAD SAFE */
 
diff -r 691a55e1aeb2 -r fa3322113480 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Wed May 12 12:20:16 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Wed May 12 12:51:32 2010 +0200
@@ -27,8 +27,6 @@
 options.isabelle.logic.title=Logic
 options.isabelle.relative-font-size.title=Relative Font Size
 options.isabelle.relative-font-size=100
-options.isabelle.relative-margin.title=Relative Margin
-options.isabelle.relative-margin=90
 options.isabelle.startup-timeout=10000
 
 #menu actions
diff -r 691a55e1aeb2 -r fa3322113480 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Wed May 12 12:51:32 2010 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.io.StringReader
-import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit}
+import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
 import java.awt.event.MouseEvent
 
 import javax.swing.{JButton, JPanel, JScrollPane}
@@ -40,13 +40,23 @@
 
 class HTML_Panel(
   sys: Isabelle_System,
-  font_size0: Int, relative_margin0: Int,
+  initial_font_size: Int,
   handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
 {
   // global logging
   Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
 
 
+  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
+
+  val screen_resolution =
+    if (GraphicsEnvironment.isHeadless()) 72
+    else Toolkit.getDefaultToolkit().getScreenResolution()
+
+  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
+  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
+
+
   /* document template */
 
   private def try_file(name: String): String =
@@ -57,14 +67,6 @@
 
   private def template(font_size: Int): String =
   {
-    // re-adjustment according to org.lobobrowser.html.style.HtmlValues.getFontSize
-    val dpi =
-      if (GraphicsEnvironment.isHeadless()) 72
-      else Toolkit.getDefaultToolkit().getScreenResolution()
-
-    val size0 = font_size * dpi / 96
-    val size = if (size0 * 96 / dpi == font_size) size0 else size0 + 1
-
     """<?xml version="1.0" encoding="utf-8"?>
 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
   "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
@@ -74,7 +76,7 @@
 """ +
   try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
   try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
-  "body { font-family: " + sys.font_family + "; font-size: " + size + "px }" +
+  "body { font-family: " + sys.font_family + "; font-size: " + raw_px(font_size) + "px }" +
 """
 </style>
 </head>
@@ -83,15 +85,13 @@
 """
   }
 
+  private def font_metrics(font_size: Int): FontMetrics =
+    Swing_Thread.now { getFontMetrics(sys.get_font(font_size)) }
 
-  def panel_width(font_size: Int, relative_margin: Int): Int =
-  {
-    val font = sys.get_font(font_size)
+  private def panel_width(font_size: Int): Int =
     Swing_Thread.now {
-      val char_width = (getFontMetrics(font).stringWidth("mix") / 3) max 1
-      ((getWidth() * relative_margin) / (100 * char_width)) max 20
+      (getWidth() / (font_metrics(font_size).charWidth(Symbol.spc) max 1) - 4) max 20
     }
-  }
 
 
   /* actor with local state */
@@ -118,8 +118,8 @@
 
   private val builder = new DocumentBuilderImpl(ucontext, rcontext)
 
-  private case class Init(font_size: Int, relative_margin: Int)
-  private case class Render(body: List[XML.Tree])
+  private case class Init(font_size: Int)
+  private case class Render(divs: List[XML.Tree])
 
   private val main_actor = actor {
     // crude double buffering
@@ -127,13 +127,13 @@
     var doc2: org.w3c.dom.Document = null
 
     var current_font_size = 16
-    var current_relative_margin = 90
+    var current_font_metrics: FontMetrics = null
 
     loop {
       react {
-        case Init(font_size, relative_margin) =>
+        case Init(font_size) =>
           current_font_size = font_size
-          current_relative_margin = relative_margin
+          current_font_metrics = font_metrics(lobo_px(raw_px(font_size)))
 
           val src = template(font_size)
           def parse() =
@@ -141,12 +141,14 @@
           doc1 = parse()
           doc2 = parse()
           Swing_Thread.now { setDocument(doc1, rcontext) }
-          
-        case Render(body) =>
+
+        case Render(divs) =>
           val doc = doc2
           val html_body =
-            Pretty.formatted(body, panel_width(current_font_size, current_relative_margin))
-              .map(t => XML.elem(HTML.PRE, HTML.spans(t)))
+            divs.flatMap(div =>
+              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())
           doc.appendChild(node)
@@ -161,9 +163,9 @@
 
 
   /* main method wrappers */
-  
-  def init(font_size: Int, relative_margin: Int) { main_actor ! Init(font_size, relative_margin) }
-  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
 
-  init(font_size0, relative_margin0)
+  def init(font_size: Int) { main_actor ! Init(font_size) }
+  def render(divs: List[XML.Tree]) { main_actor ! Render(divs) }
+
+  init(initial_font_size)
 }
diff -r 691a55e1aeb2 -r fa3322113480 src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed May 12 12:51:32 2010 +0200
@@ -16,7 +16,6 @@
 {
   private val logic_name = new JComboBox()
   private val relative_font_size = new JSpinner()
-  private val relative_margin = new JSpinner()
 
   private class List_Item(val name: String, val descr: String) {
     def this(name: String) = this(name, name)
@@ -41,11 +40,6 @@
       relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
       relative_font_size
     })
-
-    addComponent(Isabelle.Property("relative-margin.title"), {
-      relative_margin.setValue(Isabelle.Int_Property("relative-margin"))
-      relative_margin
-    })
   }
 
   override def _save()
@@ -55,8 +49,5 @@
 
     Isabelle.Int_Property("relative-font-size") =
       relative_font_size.getValue().asInstanceOf[Int]
-
-    Isabelle.Int_Property("relative-margin") =
-      relative_margin.getValue().asInstanceOf[Int]
   }
 }
diff -r 691a55e1aeb2 -r fa3322113480 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 12 12:20:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 12 12:51:32 2010 +0200
@@ -24,9 +24,7 @@
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  val html_panel =
-    new HTML_Panel(Isabelle.system,
-      Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null)
+  val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
   add(html_panel, BorderLayout.CENTER)
 
 
@@ -43,8 +41,7 @@
               html_panel.render(body)
           }
 
-        case Session.Global_Settings =>
-          html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin"))
+        case Session.Global_Settings => html_panel.init(Isabelle.font_size())
           
         case bad => System.err.println("output_actor: ignoring bad message " + bad)
       }