--- a/NEWS Wed May 12 15:27:15 2010 +0200
+++ b/NEWS Wed May 12 15:31:43 2010 +0200
@@ -73,14 +73,14 @@
discontinued (legacy feature).
* References 'trace_simp' and 'debug_simp' have been replaced by
-configuration options stored in the context. Enabling tracing
-(the case of debugging is similar) in proofs works via
-
- using [[trace_simp=true]]
-
-Tracing is then active for all invocations of the simplifier
-in subsequent goal refinement steps. Tracing may also still be
-enabled or disabled via the ProofGeneral settings menu.
+configuration options stored in the context. Enabling tracing (the
+case of debugging is similar) in proofs works via
+
+ using [[trace_simp = true]]
+
+Tracing is then active for all invocations of the simplifier in
+subsequent goal refinement steps. Tracing may also still be enabled or
+disabled via the ProofGeneral settings menu.
* Separate commands 'hide_class', 'hide_type', 'hide_const',
'hide_fact' replace the former 'hide' KIND command. Minor
@@ -89,18 +89,20 @@
*** Pure ***
-* Predicates of locales introduces by classes carry a mandatory "class"
-prefix. INCOMPATIBILITY.
-
-* 'code_reflect' allows to incorporate generated ML code into
-runtime environment; replaces immature code_datatype antiquotation.
+* Predicates of locales introduces by classes carry a mandatory
+"class" prefix. INCOMPATIBILITY.
+
+* Command 'code_reflect' allows to incorporate generated ML code into
+runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
* Empty class specifications observe default sort. INCOMPATIBILITY.
-* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
-
-* Code generator: simple concept for abstract datatypes obeying invariants.
+* Old 'axclass' command has been discontinued. Use 'class' instead.
+INCOMPATIBILITY.
+
+* Code generator: simple concept for abstract datatypes obeying
+invariants.
* Local theory specifications may depend on extra type variables that
are not present in the result type -- arguments TYPE('a) :: 'a itself
@@ -108,11 +110,12 @@
definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
-* Code generator: details of internal data cache have no impact on
-the user space functionality any longer.
-
-* Methods unfold_locales and intro_locales ignore non-locale subgoals. This
-is more appropriate for interpretations with 'where'. INCOMPATIBILITY.
+* Code generator: details of internal data cache have no impact on the
+user space functionality any longer.
+
+* Methods unfold_locales and intro_locales ignore non-locale subgoals.
+This is more appropriate for interpretations with 'where'.
+INCOMPATIBILITY.
* Discontinued unnamed infix syntax (legacy feature for many years) --
need to specify constant name and syntax separately. Internal ML
@@ -130,18 +133,18 @@
context -- without introducing dependencies on parameters or
assumptions, which is not possible in Isabelle/Pure.
-* Command 'defaultsort' is renamed to 'default_sort', it works within
-a local theory context. Minor INCOMPATIBILITY.
+* Command 'defaultsort' has been renamed to 'default_sort', it works
+within a local theory context. Minor INCOMPATIBILITY.
* Proof terms: Type substitutions on proof constants now use canonical
-order of type variables. INCOMPATIBILITY: Tools working with proof
-terms may need to be adapted.
+order of type variables. Potential INCOMPATIBILITY for tools working
+with proof terms.
*** HOL ***
-* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
-no longer shadowed. INCOMPATIBILITY.
+* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
+longer shadowed. INCOMPATIBILITY.
* Dropped theorem duplicate comp_arith; use semiring_norm instead.
INCOMPATIBILITY.
@@ -149,15 +152,15 @@
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
INCOMPATIBILITY.
-* Dropped normalizing_semiring etc; use the facts in semiring classes instead.
-INCOMPATIBILITY.
-
-* Theory 'Finite_Set': various folding_* locales facilitate the application
-of the various fold combinators on finite sets.
-
-* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
-provides abstract red-black tree type which is backed by RBT_Impl
-as implementation. INCOMPATIBILTY.
+* Dropped normalizing_semiring etc; use the facts in semiring classes
+instead. INCOMPATIBILITY.
+
+* Theory 'Finite_Set': various folding_XXX locales facilitate the
+application of the various fold combinators on finite sets.
+
+* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
+provides abstract red-black tree type which is backed by "RBT_Impl" as
+implementation. INCOMPATIBILTY.
* Command 'typedef' now works within a local theory context -- without
introducing dependencies on parameters or assumptions, which is not
@@ -171,27 +174,28 @@
* Theory PReal, including the type "preal" and related operations, has
been removed. INCOMPATIBILITY.
-* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
-Min, Max from theory Finite_Set. INCOMPATIBILITY.
-
-* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
-INCOMPATIBILITY.
-
-* New set of rules "ac_simps" provides combined assoc / commute rewrites
-for all interpretations of the appropriate generic locales.
-
-* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"
-into theories "Rings" and "Fields"; for more appropriate and more
-consistent names suitable for name prefixes within the HOL theories.
-INCOMPATIBILITY.
+* Split off theory Big_Operators containing setsum, setprod, Inf_fin,
+Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
+
+* Theory "Rational" renamed to "Rat", for consistency with "Nat",
+"Int" etc. INCOMPATIBILITY.
+
+* New set of rules "ac_simps" provides combined assoc / commute
+rewrites for all interpretations of the appropriate generic locales.
+
+* Renamed theory "OrderedGroup" to "Groups" and split theory
+"Ring_and_Field" into theories "Rings" and "Fields"; for more
+appropriate and more consistent names suitable for name prefixes
+within the HOL theories. INCOMPATIBILITY.
* Some generic constants have been put to appropriate theories:
- * less_eq, less: Orderings
- * zero, one, plus, minus, uminus, times, abs, sgn: Groups
- * inverse, divide: Rings
+ - less_eq, less: Orderings
+ - zero, one, plus, minus, uminus, times, abs, sgn: Groups
+ - inverse, divide: Rings
INCOMPATIBILITY.
-* More consistent naming of type classes involving orderings (and lattices):
+* More consistent naming of type classes involving orderings (and
+lattices):
lower_semilattice ~> semilattice_inf
upper_semilattice ~> semilattice_sup
@@ -231,8 +235,8 @@
ordered_semiring_1_strict ~> linordered_semiring_1_strict
ordered_semiring_strict ~> linordered_semiring_strict
- The following slightly odd type classes have been moved to
- a separate theory Library/Lattice_Algebras.thy:
+ The following slightly odd type classes have been moved to a
+ separate theory Library/Lattice_Algebras.thy:
lordered_ab_group_add ~> lattice_ab_group_add
lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
@@ -243,17 +247,20 @@
INCOMPATIBILITY.
* Refined field classes:
- * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
- include rule inverse 0 = 0 -- subsumes former division_by_zero class.
- * numerous lemmas have been ported from field to division_ring;
- INCOMPATIBILITY.
+ - classes division_ring_inverse_zero, field_inverse_zero,
+ linordered_field_inverse_zero include rule inverse 0 = 0 --
+ subsumes former division_by_zero class;
+ - numerous lemmas have been ported from field to division_ring.
+INCOMPATIBILITY.
* Refined algebra theorem collections:
- * dropped theorem group group_simps, use algebra_simps instead;
- * dropped theorem group ring_simps, use field_simps instead;
- * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
- * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
- INCOMPATIBILITY.
+ - dropped theorem group group_simps, use algebra_simps instead;
+ - dropped theorem group ring_simps, use field_simps instead;
+ - proper theorem collection field_simps subsumes former theorem
+ groups field_eq_simps and field_simps;
+ - dropped lemma eq_minus_self_iff which is a duplicate for
+ equal_neg_zero.
+INCOMPATIBILITY.
* Theory Finite_Set and List: some lemmas have been generalized from
sets to lattices:
@@ -279,14 +286,19 @@
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
-* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
- * pointwise ordering is instance of class order with standard syntax <= and <;
- * multiset ordering has syntax <=# and <#; partial order properties are provided
- by means of interpretation with prefix multiset_order;
- * less duplication, less historical organization of sections,
- conversion from associations lists to multisets, rudimentary code generation;
- * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
- INCOMPATIBILITY.
+* Reorganized theory Multiset: swapped notation of pointwise and
+multiset order:
+ - pointwise ordering is instance of class order with standard syntax
+ <= and <;
+ - multiset ordering has syntax <=# and <#; partial order properties
+ are provided by means of interpretation with prefix
+ multiset_order;
+ - less duplication, less historical organization of sections,
+ conversion from associations lists to multisets, rudimentary code
+ generation;
+ - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
+ if needed.
+INCOMPATIBILITY.
* Code generation: ML and OCaml code is decorated with signatures.
@@ -3317,7 +3329,7 @@
* Pure: axiomatic type classes are now purely definitional, with
explicit proofs of class axioms and super class relations performed
internally. See Pure/axclass.ML for the main internal interfaces --
-notably AxClass.define_class supersedes AxClass.add_axclass, and
+notably AxClass.define_class supercedes AxClass.add_axclass, and
AxClass.axiomatize_class/classrel/arity supersede
Sign.add_classes/classrel/arities.
@@ -4211,7 +4223,7 @@
* Pure/library.ML: the exception LIST has been given up in favour of
the standard exceptions Empty and Subscript, as well as
Library.UnequalLengths. Function like Library.hd and Library.tl are
-superseded by the standard hd and tl functions etc.
+superceded by the standard hd and tl functions etc.
A number of basic list functions are no longer exported to the ML
toplevel, as they are variants of predefined functions. The following
@@ -4342,15 +4354,15 @@
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
fold_types traverse types/terms from left to right, observing natural
-argument order. Supersedes previous foldl_XXX versions, add_frees,
+argument order. Supercedes previous foldl_XXX versions, add_frees,
add_vars etc. have been adapted as well: INCOMPATIBILITY.
* Pure: name spaces have been refined, with significant changes of the
internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table)
-to extern(_table). The plain name entry path is superseded by a
+to extern(_table). The plain name entry path is superceded by a
general 'naming' context, which also includes the 'policy' to produce
a fully qualified name and external accesses of a fully qualified
-name; NameSpace.extend is superseded by context dependent
+name; NameSpace.extend is superceded by context dependent
Sign.declare_name. Several theory and proof context operations modify
the naming context. Especially note Theory.restore_naming and
ProofContext.restore_naming to get back to a sane state; note that
@@ -4390,7 +4402,7 @@
etc.) as well as the sign field in Thm.rep_thm etc. have been retained
for convenience -- they merely return the theory.
-* Pure: type Type.tsig is superseded by theory in most interfaces.
+* Pure: type Type.tsig is superceded by theory in most interfaces.
* Pure: the Isar proof context type is already defined early in Pure
as Context.proof (note that ProofContext.context and Proof.context are
@@ -5522,7 +5534,7 @@
Eps_sym_eq -> some_sym_eq_trivial
Eps_eq -> some_eq_trivial
-* HOL: exhaust_tac on datatypes superseded by new generic case_tac;
+* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
* HOL: removed obsolete theorem binding expand_if (refer to split_if
instead);
@@ -5660,7 +5672,7 @@
replaced "delrule" by "rule del";
* Isar/Provers: new 'hypsubst' method, plain 'subst' method and
-'symmetric' attribute (the latter supersedes [RS sym]);
+'symmetric' attribute (the latter supercedes [RS sym]);
* Isar/Provers: splitter support (via 'split' attribute and 'simp'
method modifier); 'simp' method: 'only:' modifier removes loopers as
--- a/src/HOL/Library/Multiset.thy Wed May 12 15:27:15 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Wed May 12 15:31:43 2010 +0200
@@ -330,24 +330,8 @@
by (simp add: multiset_eq_conv_count_eq mset_le_def)
lemma mset_le_multiset_union_diff_commute:
- assumes "B \<le> A"
- shows "(A::'a multiset) - B + C = A + C - B"
-proof -
- from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
- from this obtain D where "A = B + D" ..
- then show ?thesis
- apply simp
- apply (subst add_commute)
- apply (subst multiset_diff_union_assoc)
- apply simp
- apply (simp add: diff_cancel)
- apply (subst add_assoc)
- apply (subst add_commute [of "B" _])
- apply (subst multiset_diff_union_assoc)
- apply simp
- apply (simp add: diff_cancel)
- done
-qed
+ "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
+by (simp add: multiset_eq_conv_count_eq mset_le_def)
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)
--- a/src/Pure/General/pretty.scala Wed May 12 15:27:15 2010 +0200
+++ b/src/Pure/General/pretty.scala Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Pure/General/symbol.scala Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Pure/General/xml.scala Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed May 12 15:31:43 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 15:27:15 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 12 15:31:43 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)
}