# 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", "\\", "\\<^newline>") + Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\", "\\<^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 - """ @@ -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 @@ """ } + 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) }