# HG changeset patch
# User wenzelm
# Date 1364043466 -3600
# Node ID 59d8a1031c00a409b7338a22beba6c708475494c
# Parent  eaa1c4cc11068264bb1923305978ce1f0c882c59
allow fractional pretty margin -- avoid premature rounding;

diff -r eaa1c4cc1106 -r 59d8a1031c00 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Mar 23 13:12:39 2013 +0100
+++ b/src/Pure/General/pretty.scala	Sat Mar 23 13:57:46 2013 +0100
@@ -89,9 +89,9 @@
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
-  private val margin_default = 76
+  private val margin_default = 76.0
 
-  def formatted(input: XML.Body, margin: Int = margin_default,
+  def formatted(input: XML.Body, margin: Double = margin_default,
     metric: Metric = Metric_Default): XML.Body =
   {
     sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
@@ -162,7 +162,7 @@
     format(standard_format(input), 0.0, 0.0, Text()).content
   }
 
-  def string_of(input: XML.Body, margin: Int = margin_default,
+  def string_of(input: XML.Body, margin: Double = margin_default,
       metric: Metric = Metric_Default): String =
     XML.content(formatted(input, margin, metric))
 
diff -r eaa1c4cc1106 -r 59d8a1031c00 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 23 13:12:39 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Mar 23 13:57:46 2013 +0100
@@ -201,7 +201,8 @@
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
                 val info_text =
-                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
+                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
+                    .mkString
 
                 new DefaultMutableTreeNode(
                   new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
diff -r eaa1c4cc1106 -r 59d8a1031c00 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 13:12:39 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Mar 23 13:57:46 2013 +0100
@@ -109,7 +109,7 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.pretty_metric(getPainter)
-      val margin = (getPainter.getWidth.toDouble / metric.unit).toInt max 20
+      val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
 
       val base_snapshot = current_base_snapshot
       val base_results = current_base_results
diff -r eaa1c4cc1106 -r 59d8a1031c00 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 13:12:39 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 23 13:57:46 2013 +0100
@@ -191,7 +191,7 @@
     {
       val painter = pretty_text_area.getPainter
       val metric = JEdit_Lib.pretty_metric(painter)
-      val margin = (rendering.tooltip_margin * metric.average).toInt
+      val margin = rendering.tooltip_margin * metric.average
       val lines =
         XML.traverse_text(Pretty.formatted(body, margin, metric))(0)(
           (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
@@ -208,7 +208,7 @@
 
       val bounds = rendering.tooltip_bounds
       val w =
-        ((metric.unit * (margin + 1)).round.toInt + deco_width) min
+        ((metric.unit * (margin + metric.average)).round.toInt + deco_width) min
         (screen_bounds.width * bounds).toInt
       val h =
         (painter.getFontMetrics.getHeight * (lines + 1) + deco_height) min