# HG changeset patch
# User wenzelm
# Date 1353248938 -3600
# Node ID 32755e357a51d59232ea26a1bbf4b62f365ddc01
# Parent  88b971fca902944b5895731d82a4fcd77d1c4ffb
update options via protocol;
jEdit dialog for "Parallel Checking" options;

diff -r 88b971fca902 -r 32755e357a51 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sun Nov 18 15:28:58 2012 +0100
@@ -198,13 +198,8 @@
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     val _ = Output.physical_stderr Symbol.STX;
 
-    (* FIXME proper system options *)
     val _ = Printer.show_markup_default := true;
     val _ = quick_and_dirty := false;
-    val _ = Goal.parallel_proofs := 4;
-    val _ =
-      if Multithreading.max_threads_value () < 2
-      then Multithreading.max_threads := 2 else ();
     val _ = Context.set_thread_data NONE;
     val _ =
       Unsynchronized.change print_mode
@@ -217,5 +212,20 @@
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
 fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);
 
+
+(* options *)
+
+val _ =
+  protocol_command "Isabelle_Process.options"
+    (fn [options_yxml] =>
+      let val options = Options.decode (YXML.parse_body options_yxml) in
+        Multithreading.trace := Options.int options "threads_trace";
+        Multithreading.max_threads := Options.int options "threads";
+        if Multithreading.max_threads_value () < 2
+        then Multithreading.max_threads := 2 else ();
+        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
+        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold"
+      end);
+
 end;
 
diff -r 88b971fca902 -r 32755e357a51 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -393,11 +393,18 @@
   def input_bytes(name: String, args: Array[Byte]*): Unit =
     command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
 
-  def input(name: String, args: String*): Unit =
+  def input(name: String, args: String*)
   {
     receiver(new Input(name, args.toList))
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
   }
 
-  def close_input(): Unit = { close(command_input); close(standard_input) }
+  def options(opts: Options): Unit =
+    input("Isabelle_Process.options", YXML.string_of_body(opts.encode))
+
+  def close_input()
+  {
+    close(command_input)
+    close(standard_input)
+  }
 }
diff -r 88b971fca902 -r 32755e357a51 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Pure/System/session.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -22,7 +22,7 @@
   /* events */
 
   //{{{
-  case object Global_Options
+  case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(edits: List[Document.Edit_Text])
   case class Commands_Changed(
@@ -58,7 +58,7 @@
 
   /* pervasive event buses */
 
-  val global_options = new Event_Bus[Session.Global_Options.type]
+  val global_options = new Event_Bus[Session.Global_Options]
   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   val raw_edits = new Event_Bus[Session.Raw_Edits]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
@@ -397,6 +397,9 @@
           receiver.cancel()
           reply(())
 
+        case Session.Global_Options(options) if prover.isDefined =>
+          prover.get.options(options)
+
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
 
@@ -444,9 +447,18 @@
   /* actions */
 
   def start(args: List[String])
-  { session_actor ! Start(args) }
+  {
+    global_options += session_actor
+    session_actor ! Start(args)
+  }
 
-  def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
+  def stop()
+  {
+    global_options -= session_actor
+    commands_changed_buffer !? Stop
+    change_parser !? Stop
+    session_actor !? Stop
+  }
 
   def cancel_execution() { session_actor ! Cancel_Execution }
 
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -105,7 +105,7 @@
   private val main_actor = actor {
     loop {
       react {
-        case Session.Global_Options =>  // FIXME
+        case _: Session.Global_Options =>  // FIXME
 
         case changed: Session.Commands_Changed =>
           Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -86,7 +86,7 @@
   private val main_actor = actor {
     loop {
       react {
-        case Session.Global_Options =>
+        case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
         case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
       }
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -42,7 +42,8 @@
   // FIXME avoid hard-wired stuff
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit",
-      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "editor_load_delay",
+      "jedit_tooltip_font_scale", "jedit_tooltip_margin", "threads", "threads_trace",
+      "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay",
       "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -101,7 +101,7 @@
   private val main_actor = actor {
     loop {
       react {
-        case Session.Global_Options =>
+        case _: Session.Global_Options =>
           Swing_Thread.later { handle_resize() }
         case changed: Session.Commands_Changed =>
           Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -296,7 +296,7 @@
           }
 
         case msg: PropertiesChanged =>
-          Isabelle.session.global_options.event(Session.Global_Options)
+          Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
 
         case _ =>
       }
diff -r 88b971fca902 -r 32755e357a51 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 18 14:24:30 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 18 15:28:58 2012 +0100
@@ -150,7 +150,7 @@
       react {
         case phase: Session.Phase => handle_phase(phase)
 
-        case Session.Global_Options => Swing_Thread.later { logic.load () }
+        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))