src/Tools/jEdit/src/isabelle_options.scala
changeset 52065 78f2475aa126
parent 51554 041bc3d31f23
child 56559 eece73c31e38
equal deleted inserted replaced
52064:4b4ff1d3b723 52065:78f2475aa126
    37 }
    37 }
    38 
    38 
    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   val options = PIDE.options
    43   private val relevant_options =
       
    44     Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
       
    45       "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_delay",
       
    46       "jedit_tooltip_font_scale", "jedit_tooltip_margin", "jedit_mac_adapter",
       
    47       "jedit_timing_threshold", "threads", "threads_trace", "parallel_proofs",
       
    48       "parallel_subproofs_saturation", "editor_skip_proofs", "editor_load_delay",
       
    49       "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
       
    50       "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
       
    51 
       
    52   relevant_options.foreach(PIDE.options.value.check_name _)
       
    53 
       
    54   protected val components =
    43   protected val components =
    55     PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
    44     options.make_components(List(Isabelle_Logic.logic_selector(false)),
       
    45       (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
    56 }
    46 }
    57 
    47 
    58 
    48 
    59 class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
    49 class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
    60 {
    50 {
    61   // FIXME avoid hard-wired stuff
       
    62   private val predefined =
    51   private val predefined =
    63     (for {
    52     (for {
    64       (name, opt) <- PIDE.options.value.options.toList
    53       (name, opt) <- PIDE.options.value.options.toList
    65       if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
    54       if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
    66     } yield PIDE.options.make_color_component(opt))
    55     } yield PIDE.options.make_color_component(opt))
    67 
    56 
    68   assert(!predefined.isEmpty)
    57   assert(!predefined.isEmpty)
    69 
    58 
    70   protected val components = PIDE.options.make_components(predefined, _ => false)
    59   protected val components = PIDE.options.make_components(predefined, _ => false)