src/Tools/jEdit/src/isabelle_options.scala
changeset 51423 e5f9a6d9ca82
parent 51071 b7e7557e80b5
child 51441 37f699750430
equal deleted inserted replaced
51422:821a70e29e0b 51423:e5f9a6d9ca82
    39 
    39 
    40 class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
    40 class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
    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",
    45       "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
    45       "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
    46       "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
    46       "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
    47       "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
    47       "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
    48       "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
    48       "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
    49       "editor_update_delay", "editor_chart_delay")
    49       "editor_update_delay", "editor_chart_delay")
    50 
    50 
    51   relevant_options.foreach(PIDE.options.value.check_name _)
    51   relevant_options.foreach(PIDE.options.value.check_name _)
    52 
    52