clarified;
authorwenzelm
Fri, 21 Dec 2018 13:38:44 +0100
changeset 69505 6fa742b03107
parent 69504 b4b4d3ec55b3
child 69506 7e44f8e2cc49
clarified;
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
 }