# HG changeset patch
# User wenzelm
# Date 1598534216 -7200
# Node ID 0d7cd97f6c484acc925d3472de8fa08a33809f14
# Parent  8f9cffa78112959a97178ebe906568886b03f7cc
clarified treatment of add-on prover_options;

diff -r 8f9cffa78112 -r 0d7cd97f6c48 src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Thu Aug 27 13:06:58 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Thu Aug 27 15:16:56 2020 +0200
@@ -74,6 +74,10 @@
 {
   private val state = Synchronized(Protocol_Handlers.State(session))
 
+  def prover_options(options: Options): Options =
+    (options /: state.value.handlers)(
+      { case (opts, (_, handler)) => handler.prover_options(opts) })
+
   def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
   def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
   def init(name: String): Unit = state.change(_.init(name))
diff -r 8f9cffa78112 -r 0d7cd97f6c48 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Aug 27 13:06:58 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Aug 27 15:16:56 2020 +0200
@@ -118,6 +118,7 @@
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
     def functions: List[(String, Protocol_Function)] = Nil
+    def prover_options(options: Options): Options = options
   }
 }
 
@@ -353,14 +354,11 @@
   }
 
 
-  /* file formats */
+  /* file formats and protocol handlers */
 
-  lazy val file_formats: File_Format.Session =
+  private lazy val file_formats: File_Format.Session =
     File_Format.registry.start_session(session)
 
-
-  /* protocol handlers */
-
   private val protocol_handlers = Protocol_Handlers.init(session)
 
   def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] =
@@ -372,6 +370,9 @@
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
+  def prover_options(options: Options): Options =
+    protocol_handlers.prover_options(file_formats.prover_options(options))
+
 
   /* debugger */
 
@@ -543,12 +544,12 @@
               change_command(_.accumulate(state_id, output.message, xml_cache))
 
             case _ if output.is_init =>
-              prover.get.options(file_formats.prover_options(session_options))
-              prover.get.init_session(resources)
-
               Isabelle_System.make_services(classOf[Session.Protocol_Handler])
                 .foreach(init_protocol_handler)
 
+              prover.get.options(prover_options(session_options))
+              prover.get.init_session(resources)
+
               phase = Session.Ready
               debugger.ready()
 
@@ -625,7 +626,7 @@
 
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
-              prover.get.options(file_formats.prover_options(options))
+              prover.get.options(prover_options(options))
               handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))