--- 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)
}
--- 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("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
--- 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 */
--- 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
--- 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)
}
--- 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]
}
}
--- 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)
}