support Isabelle plugin properties with defaults;
font size relative to view.textsize of jEdit;
margin relative to component width and approximative font metrics;

--- 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

--- 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)
 }

--- 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]
   }
 }

--- 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)
       }

--- 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 */