# HG changeset patch
# User wenzelm
# Date 1545395924 -3600
# Node ID 6fa742b0310753db08e35b83fb2072b2b9dbfd3d
# Parent  b4b4d3ec55b31e606ccd4c3fd266a2ac9f9d4f5b
clarified;

diff -r b4b4d3ec55b3 -r 6fa742b03107 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Fri Dec 21 13:33:56 2018 +0100
+++ b/src/Pure/Thy/file_format.scala	Fri Dec 21 13:38:44 2018 +0100
@@ -27,7 +27,7 @@
     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)))
+      new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
   }
 
 
@@ -50,10 +50,7 @@
     def stop {}
   }
 
-  object Agent extends Agent
-  {
-    override def toString: String = "-"
-  }
+  object No_Agent extends Agent
 }
 
 trait File_Format
@@ -96,5 +93,5 @@
 
   /* PIDE session agent */
 
-  def start(session: isabelle.Session): File_Format.Agent = File_Format.Agent
+  def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent
 }