41 { |
41 { |
42 // FIXME avoid hard-wired stuff |
42 // FIXME avoid hard-wired stuff |
43 private val relevant_options = |
43 private val relevant_options = |
44 Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit", |
44 Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit", |
45 "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin", |
45 "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin", |
46 "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", |
46 "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs", |
47 "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit", |
47 "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay", |
48 "editor_tracing_messages", "editor_update_delay", "editor_chart_delay") |
48 "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages", |
|
49 "editor_update_delay", "editor_chart_delay") |
49 |
50 |
50 relevant_options.foreach(PIDE.options.value.check_name _) |
51 relevant_options.foreach(PIDE.options.value.check_name _) |
51 |
52 |
52 protected val components = |
53 protected val components = |
53 PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options) |
54 PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options) |