Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more flexibile font size via CSS <style> instead of old <font> element;
authorwenzelm
Mon, 31 May 2010 09:47:41 +0200
changeset 37203 c4261f3bbdd7
parent 37202 382a56c9f295
child 37204 12d850a27eef
more flexibile font size via CSS <style> instead of old <font> element; preformatted text;
src/Tools/jEdit/plugin/Isabelle.props file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/jedit/isabelle_options.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/jedit/plugin.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/plugin/Isabelle.props	Mon May 31 09:46:43 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Mon May 31 09:47:41 2010 +0200
@@ -28,7 +28,7 @@
 options.isabelle.relative-font-size.title=Relative Font Size
 options.isabelle.relative-font-size=100
 options.isabelle.tooltip-font-size.title=Tooltip Font Size
-options.isabelle.tooltip-font-size=4
+options.isabelle.tooltip-font-size=10
 options.isabelle.startup-timeout=10000
 
 #menu actions
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Mon May 31 09:46:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Mon May 31 09:47:41 2010 +0200
@@ -43,7 +43,7 @@
     })
 
     addComponent(Isabelle.Property("tooltip-font-size.title"), {
-      tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 4))
+      tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
       tooltip_font_size
     })
   }
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon May 31 09:46:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Mon May 31 09:47:41 2010 +0200
@@ -83,16 +83,10 @@
 
   /* tooltip markup */
 
-  // raw font markup
-
-  def font(name: String, size: Int, body: List[XML.Tree]): XML.Tree =
-    XML.Elem("font", List(("face", name), ("size", size.toString)), body)
-
-
   def tooltip(text: String): String =
-    "<html><font face=\"" + font_family() + "\" size=\"" +
-        Int_Property("tooltip-font-size", 4).toString + "\">" +
-      HTML.encode(text) + "</font></html>"
+    "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
+        Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
+      HTML.encode(text) + "</pre></html>"
 
 
   /* settings */
isabelle