# HG changeset patch # User wenzelm # Date 1273585651 -7200 # Node ID dc85664dbf6d0b74a2398b7890e8dfae453b3720 # Parent 4cf53796401060c7f0b6c76fe29503aa35b12fcb support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics; diff -r 4cf537964010 -r dc85664dbf6d src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 10:36:50 2010 +0200 +++ b/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 15:47:31 2010 +0200 @@ -25,8 +25,10 @@ options.isabelle.label=Isabelle options.isabelle.code=new isabelle.jedit.Isabelle_Options(); options.isabelle.logic.title=Logic -options.isabelle.font-size.title=Font Size -options.isabelle.font-size=14 +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 4cf537964010 -r dc85664dbf6d src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 10:36:50 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 15:47:31 2010 +0200 @@ -40,7 +40,7 @@ class HTML_Panel( sys: Isabelle_System, - initial_font_size: Int, + font_size0: Int, relative_margin0: Int, handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel { // global logging @@ -84,6 +84,16 @@ } + def panel_width(font_size: Int, relative_margin: Int): Int = + { + val font = sys.get_font(font_size) + Swing_Thread.now { + val char_width = (getFontMetrics(font).stringWidth("mix") / 3) max 1 + ((getWidth() * relative_margin) / (100 * char_width)) max 20 + } + } + + /* actor with local state */ private val ucontext = new SimpleUserAgentContext @@ -108,7 +118,7 @@ private val builder = new DocumentBuilderImpl(ucontext, rcontext) - private case class Init(font_size: Int) + private case class Init(font_size: Int, relative_margin: Int) private case class Render(body: List[XML.Tree]) private val main_actor = actor { @@ -116,9 +126,15 @@ var doc1: org.w3c.dom.Document = null var doc2: org.w3c.dom.Document = null + var current_font_size = 16 + var current_relative_margin = 90 + loop { react { - case Init(font_size) => + case Init(font_size, relative_margin) => + current_font_size = font_size + current_relative_margin = relative_margin + val src = template(font_size) def parse() = builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost")) @@ -128,7 +144,9 @@ case Render(body) => val doc = doc2 - val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t))) + val html_body = + Pretty.formatted(body, panel_width(current_font_size, current_relative_margin)) + .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) @@ -141,11 +159,11 @@ } } - main_actor ! Init(initial_font_size) - /* main method wrappers */ - def init(font_size: Int) { main_actor ! Init(font_size) } + 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) } diff -r 4cf537964010 -r dc85664dbf6d src/Tools/jEdit/src/jedit/isabelle_options.scala --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 10:36:50 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 15:47:31 2010 +0200 @@ -15,7 +15,8 @@ class Isabelle_Options extends AbstractOptionPane("isabelle") { private val logic_name = new JComboBox() - private val font_size = new JSpinner() + 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) @@ -36,18 +37,26 @@ logic_name }) - addComponent(Isabelle.Property("font-size.title"), { - font_size.setValue(Isabelle.Int_Property("font-size")) - font_size + addComponent(Isabelle.Property("relative-font-size.title"), { + 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() { - val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name - Isabelle.Property("logic") = logic + Isabelle.Property("logic") = + logic_name.getSelectedItem.asInstanceOf[List_Item].name - val size = font_size.getValue().asInstanceOf[Int] - Isabelle.Int_Property("font-size") = size + Isabelle.Int_Property("relative-font-size") = + relative_font_size.getValue().asInstanceOf[Int] + + Isabelle.Int_Property("relative-margin") = + relative_margin.getValue().asInstanceOf[Int] } } diff -r 4cf537964010 -r dc85664dbf6d src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 10:36:50 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 15:47:31 2010 +0200 @@ -24,8 +24,9 @@ if (position == DockableWindowManager.FLOATING) setPreferredSize(new Dimension(500, 250)) - private val html_panel = - new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null) + val html_panel = + new HTML_Panel(Isabelle.system, + Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null) add(html_panel, BorderLayout.CENTER) @@ -43,7 +44,7 @@ } case Session.Global_Settings => - html_panel.init(Isabelle.Int_Property("font-size")) + html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin")) case bad => System.err.println("output_actor: ignoring bad message " + bad) } diff -r 4cf537964010 -r dc85664dbf6d src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Tue May 11 10:36:50 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue May 11 15:47:31 2010 +0200 @@ -42,22 +42,37 @@ object Property { - def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name) - def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value) + def apply(name: String): String = + jEdit.getProperty(OPTION_PREFIX + name) + def apply(name: String, default: String): String = + jEdit.getProperty(OPTION_PREFIX + name, default) + def update(name: String, value: String) = + jEdit.setProperty(OPTION_PREFIX + name, value) } object Boolean_Property { - def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name) - def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value) + def apply(name: String): Boolean = + jEdit.getBooleanProperty(OPTION_PREFIX + name) + def apply(name: String, default: Boolean): Boolean = + jEdit.getBooleanProperty(OPTION_PREFIX + name, default) + def update(name: String, value: Boolean) = + jEdit.setBooleanProperty(OPTION_PREFIX + name, value) } object Int_Property { - def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name) - def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value) + def apply(name: String): Int = + jEdit.getIntegerProperty(OPTION_PREFIX + name) + def apply(name: String, default: Int): Int = + jEdit.getIntegerProperty(OPTION_PREFIX + name, default) + def update(name: String, value: Int) = + jEdit.setIntegerProperty(OPTION_PREFIX + name, value) } + def font_size(): Int = + (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100 + /* settings */