--- a/src/Tools/jEdit/etc/options Fri May 17 23:31:02 2013 +0200
+++ b/src/Tools/jEdit/etc/options Sat May 18 12:41:31 2013 +0200
@@ -1,33 +1,33 @@
(* :mode=isabelle-options: *)
-option jedit_logic : string = ""
+public option jedit_logic : string = ""
-- "default logic session"
-option jedit_font_scale : real = 1.0
+public option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
-option jedit_tooltip_delay : real = 0.75
+public option jedit_tooltip_delay : real = 0.75
-- "open/close delay for document tooltips"
-option jedit_tooltip_font_scale : real = 0.85
+public option jedit_tooltip_font_scale : real = 0.85
-- "scale factor of tooltips wrt. main text area"
-option jedit_tooltip_margin : int = 60
+public option jedit_tooltip_margin : int = 60
-- "margin for tooltip pretty-printing"
-option jedit_tooltip_bounds : real = 0.5
+public option jedit_tooltip_bounds : real = 0.5
-- "relative bounds of tooltip window wrt. logical screen size"
-option jedit_text_overview_limit : int = 100000
+public option jedit_text_overview_limit : int = 100000
-- "maximum amount of text to visualize in overview column"
-option jedit_symbols_search_limit : int = 50
+public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-option jedit_mac_adapter : bool = true
+public option jedit_mac_adapter : bool = true
-- "some native Mac OS X support (potential conflict with MacOSX plugin)"
-option jedit_timing_threshold : real = 0.1
+public option jedit_timing_threshold : real = 0.1
-- "default threshold for timing display"