| changeset 69489 | 18c58b0da0a9 |
| parent 69488 | b05c0bb47f6d |
| child 69493 | 6fa742b03107 |
--- 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 }