# HG changeset patch
# User wenzelm
# Date 1448130426 -3600
# Node ID 1529c3eb6bac44a049aef2c227bfc5e564d2d8ad
# Parent  4bfcc09a33e800c7b16705ba026761d9683866b1
more thorough update of options;

diff -r 4bfcc09a33e8 -r 1529c3eb6bac src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Sat Nov 21 19:04:39 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Nov 21 19:27:06 2015 +0100
@@ -187,8 +187,7 @@
     GUI_Thread.require {
       if (continuous_checking != b) {
         PIDE.options.bool(CONTINUOUS_CHECKING) = b
-        PIDE.options_changed()
-        PIDE.editor.flush()
+        PIDE.session.update_options(PIDE.options.value)
       }
     }
 
diff -r 4bfcc09a33e8 -r 1529c3eb6bac src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Nov 21 19:04:39 2015 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Nov 21 19:27:06 2015 +0100
@@ -90,8 +90,7 @@
   {
     if (output_state != b) {
       PIDE.options.bool("editor_output_state") = b
-      PIDE.options_changed()
-      PIDE.editor.flush()
+      PIDE.session.update_options(PIDE.options.value)
     }
   }