# HG changeset patch # User wenzelm # Date 1273613766 -7200 # Node ID ed97e877ff2d920a055a71a48e2b93f06a085f80 # Parent da7628b3d231742fb971f5be1758a7846b1f0e8a more precise pretty printing based on actual font metrics; removed obsolete relative margin; diff -r da7628b3d231 -r ed97e877ff2d src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Tue May 11 23:09:49 2010 +0200 +++ b/src/Pure/General/pretty.scala Tue May 11 23:36:06 2010 +0200 @@ -45,32 +45,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 +53,47 @@ Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString))) } + 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 + } + private val margin_default = 76 - def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] = + def formatted(input: List[XML.Tree], margin: Int = margin_default, + metric: String => Double = (_.length.toDouble)): 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 XML.Elem(_, _, body) :: ts => + (0.0 /: body)(_ + content_length(_)) + breakdist(ts, after) + case XML.Text(s) :: ts => metric(s) + 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,17 +110,17 @@ 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 = @@ -128,7 +135,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 da7628b3d231 -r ed97e877ff2d src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Tue May 11 23:09:49 2010 +0200 +++ b/src/Pure/General/xml.scala Tue May 11 23:36:06 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 da7628b3d231 -r ed97e877ff2d src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 23:09:49 2010 +0200 +++ b/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 23:36:06 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 da7628b3d231 -r ed97e877ff2d src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 23:09:49 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 23:36:06 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 - """ @@ -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 }" + """ @@ -83,15 +85,13 @@ """ } + 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) + 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,7 +118,7 @@ private val builder = new DocumentBuilderImpl(ucontext, rcontext) - private case class Init(font_size: Int, relative_margin: Int) + private case class Init(font_size: Int) private case class Render(body: List[XML.Tree]) private val main_actor = actor { @@ -127,13 +127,17 @@ var doc2: org.w3c.dom.Document = null var current_font_size = 16 - var current_relative_margin = 90 + 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, 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,11 +145,11 @@ doc1 = parse() doc2 = parse() Swing_Thread.now { setDocument(doc1, rcontext) } - + case Render(body) => val doc = doc2 val html_body = - Pretty.formatted(body, panel_width(current_font_size, current_relative_margin)) + Pretty.formatted(body, panel_width(current_font_size), metric) .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()) @@ -161,9 +165,9 @@ /* main method wrappers */ - - def init(font_size: Int, relative_margin: Int) { main_actor ! Init(font_size, relative_margin) } + + def init(font_size: Int) { main_actor ! Init(font_size) } def render(body: List[XML.Tree]) { main_actor ! Render(body) } - init(font_size0, relative_margin0) + init(initial_font_size) } diff -r da7628b3d231 -r ed97e877ff2d src/Tools/jEdit/src/jedit/isabelle_options.scala --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 23:09:49 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 23:36:06 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 da7628b3d231 -r ed97e877ff2d src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 23:09:49 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 23:36:06 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) }