# HG changeset patch
# User wenzelm
# Date 1545343537 -3600
# Node ID b05c0bb47f6d6b1a464770fa4f9d78c9788fabb7
# Parent  681760f50723585d8cf6d59cc8f03c96ae68c846
support for File_Format.Session, e.g. server process accessible via prover options;

diff -r 681760f50723 -r b05c0bb47f6d src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Dec 20 22:56:36 2018 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Dec 20 23:05:37 2018 +0100
@@ -343,6 +343,12 @@
   }
 
 
+  /* file formats */
+
+  lazy val file_formats: File_Format.Session =
+    resources.file_formats.start_session(session)
+
+
   /* protocol handlers */
 
   private val protocol_handlers = Protocol_Handlers.init(session)
@@ -513,12 +519,13 @@
               change_command(_.accumulate(state_id, output.message, xml_cache))
 
             case _ if output.is_init =>
-              prover.get.options(session_options)
+              prover.get.options(file_formats.prover_options(session_options))
               prover.get.session_base(resources)
               phase = Session.Ready
               debugger.ready()
 
             case Markup.Process_Result(result) if output.is_exit =>
+              file_formats.stop_session
               phase = Session.Terminated(result)
               prover.reset
 
@@ -587,7 +594,7 @@
 
           case Update_Options(options) =>
             if (prover.defined && is_ready) {
-              prover.get.options(options)
+              prover.get.options(file_formats.prover_options(options))
               handle_raw_edits()
             }
             global_options.post(Session.Global_Options(options))
@@ -633,6 +640,7 @@
 
   def start(start_prover: Prover.Receiver => Prover)
   {
+    file_formats
     _phase.change(
       {
         case Session.Inactive =>
diff -r 681760f50723 -r b05c0bb47f6d src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Thu Dec 20 22:56:36 2018 +0100
+++ b/src/Pure/Thy/file_format.scala	Thu Dec 20 23:05:37 2018 +0100
@@ -9,6 +9,11 @@
 
 object File_Format
 {
+  sealed case class Theory_Context(name: Document.Node.Name, content: String)
+
+
+  /* environment */
+
   def environment(): Environment =
     new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
 
@@ -20,9 +25,35 @@
     def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
     def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
     def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
+
+    def start_session(session: isabelle.Session): Session =
+      new Session(file_formats.map(_.start(session)))
   }
 
-  sealed case class Theory_Context(name: Document.Node.Name, content: String)
+
+  /* session */
+
+  final class Session private[File_Format](agents: List[Agent])
+  {
+    override def toString: String =
+      agents.mkString("File_Format.Session(", ", ", ")")
+
+    def prover_options(options: Options): Options =
+      (options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
+
+    def stop_session { agents.foreach(_.stop) }
+  }
+
+  trait Agent
+  {
+    def prover_options(options: Options): Options = options
+    def stop {}
+  }
+
+  object Agent extends Agent
+  {
+    override def toString: String = "-"
+  }
 }
 
 trait File_Format
@@ -61,4 +92,9 @@
   }
 
   def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
+
+
+  /* PIDE session */
+
+  def start(session: isabelle.Session): File_Format.Agent = File_Format.Agent
 }