# HG changeset patch
# User wenzelm
# Date 1545392310 -3600
# Node ID 18c58b0da0a92f5e1cb6df1bbdabc6ae5a8754a4
# Parent  b05c0bb47f6d6b1a464770fa4f9d78c9788fabb7
tuned comments;

diff -r b05c0bb47f6d -r 18c58b0da0a9 src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Thu Dec 20 23:05:37 2018 +0100
+++ b/src/Pure/Thy/file_format.scala	Fri Dec 21 12:38:30 2018 +0100
@@ -94,7 +94,7 @@
   def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
 
 
-  /* PIDE session */
+  /* PIDE session agent */
 
   def start(session: isabelle.Session): File_Format.Agent = File_Format.Agent
 }