equal
deleted
inserted
replaced
40 class Isabelle_Options1 extends Isabelle_Options("isabelle-general") |
40 class Isabelle_Options1 extends Isabelle_Options("isabelle-general") |
41 { |
41 { |
42 val options = PIDE.options |
42 val options = PIDE.options |
43 |
43 |
44 private val predefined = |
44 private val predefined = |
45 List(JEdit_Sessions.logic_selector(false), JEdit_Spell_Checker.dictionaries_selector()) |
45 List(JEdit_Sessions.logic_selector(options.value, false), |
|
46 JEdit_Spell_Checker.dictionaries_selector()) |
46 |
47 |
47 protected val components = |
48 protected val components = |
48 options.make_components(predefined, |
49 options.make_components(predefined, |
49 (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet) |
50 (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet) |
50 } |
51 } |