# HG changeset patch
# User wenzelm
# Date 1503252336 -7200
# Node ID f7b0d6fb417a15db847765f7385989fc0d8272c7
# Parent  b578ef1a8b4057b38fc8b8342c9c12a98fba5631
proper update of options (amending c3d6dd17d626);

diff -r b578ef1a8b40 -r f7b0d6fb417a src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Aug 20 18:45:42 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Aug 20 20:05:36 2017 +0200
@@ -42,7 +42,7 @@
   val options = PIDE.options
 
   private val predefined =
-    List(JEdit_Sessions.logic_selector(options.value, false),
+    List(JEdit_Sessions.logic_selector(options, false),
       JEdit_Spell_Checker.dictionaries_selector())
 
   protected val components =
diff -r b578ef1a8b40 -r f7b0d6fb417a src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Aug 20 18:45:42 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sun Aug 20 20:05:36 2017 +0200
@@ -100,13 +100,13 @@
     override def toString: String = description
   }
 
-  def logic_selector(options: Options, autosave: Boolean): Option_Component =
+  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
   {
     GUI_Thread.require {}
 
     val entries =
-      new Logic_Entry("", "default (" + session_name(options) + ")") ::
-        session_list(options).map(name => new Logic_Entry(name, name))
+      new Logic_Entry("", "default (" + session_name(options.value) + ")") ::
+        session_list(options.value).map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
diff -r b578ef1a8b40 -r f7b0d6fb417a src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Aug 20 18:45:42 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sun Aug 20 20:05:36 2017 +0200
@@ -86,7 +86,7 @@
   private val continuous_checking = new Isabelle.Continuous_Checking
   continuous_checking.focusable = false
 
-  private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true)
+  private val logic = JEdit_Sessions.logic_selector(PIDE.options, true)
 
   private val controls =
     Wrap_Panel(List(purge, continuous_checking, session_phase, logic))