src/Tools/jEdit/src/isabelle_options.scala
changeset 50117 32755e357a51
parent 49969 72216713733a
child 50119 5c370a036de7
equal deleted inserted replaced
50116:88b971fca902 50117:32755e357a51
    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_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
    44     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
    45       "jedit_tooltip_font_scale", "jedit_tooltip_margin", "editor_load_delay",
    45       "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
       
    46       "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
    46       "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
    47       "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
    47 
    48 
    48   relevant_options.foreach(Isabelle.options.value.check_name _)
    49   relevant_options.foreach(Isabelle.options.value.check_name _)
    49 
    50 
    50   protected val components =
    51   protected val components =