--- a/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 15:59:35 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 16:10:54 2012 +0200
@@ -16,9 +16,11 @@
{
// FIXME avoid hard-wired stuff
private val relevant_options =
- Set("jedit_logic", "jedit_auto_start", "jedit_relative_font_size", "jedit_tooltip_font_size",
+ Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
"jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay")
+ relevant_options.foreach(Isabelle.options.value.check_name _)
+
private val components =
Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)