# HG changeset patch # User haftmann # Date 1273671103 -7200 # Node ID 8160596aeb65518facd06d32c31093dd074e9cf5 # Parent b78d3c87fc889c5012b191a1c2e083272fe49f83# Parent 112e613e8d0b100bdc309bdf1e0861322ac88374 merged diff -r 112e613e8d0b -r 8160596aeb65 NEWS --- 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 diff -r 112e613e8d0b -r 8160596aeb65 src/HOL/Library/Multiset.thy --- 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 \ A" - shows "(A::'a multiset) - B + C = A + C - B" -proof - - from mset_le_exists_conv [of "B" "A"] assms have "\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 \ A \ (A::'a multiset) - B + C = A + C - B" +by (simp add: multiset_eq_conv_count_eq mset_le_def) lemma mset_lessD: "A < B \ x \# A \ x \# B" apply (clarsimp simp: mset_le_def mset_less_def) diff -r 112e613e8d0b -r 8160596aeb65 src/Pure/General/pretty.scala --- 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) } diff -r 112e613e8d0b -r 8160596aeb65 src/Pure/General/symbol.scala --- 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", "\\", "\\<^newline>") + Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\", "\\<^newline>") private val sym_chars = Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~") diff -r 112e613e8d0b -r 8160596aeb65 src/Pure/General/xml.scala --- 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 */ diff -r 112e613e8d0b -r 8160596aeb65 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 112e613e8d0b -r 8160596aeb65 src/Tools/jEdit/src/jedit/html_panel.scala --- 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 - """ @@ -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 112e613e8d0b -r 8160596aeb65 src/Tools/jEdit/src/jedit/isabelle_options.scala --- 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] } } diff -r 112e613e8d0b -r 8160596aeb65 src/Tools/jEdit/src/jedit/output_dockable.scala --- 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) }