# HG changeset patch
# User wenzelm
# Date 1660991977 -7200
# Node ID 16a53676ebbdf9abccd1d2dcab07b56a98569310
# Parent  20b918404aa36167e1ae464bb48f1c3e73ed63a0
tuned whitespace;

diff -r 20b918404aa3 -r 16a53676ebbd src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 20 00:24:04 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 20 12:39:37 2022 +0200
@@ -420,9 +420,9 @@
         if matcher(entry_name)
         entry <- get(entry_name.theory, entry_name.name).iterator
       } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
-  }
+    }
 
-  override def toString: String =
+    override def toString: String =
       "Export.Session_Context(" + commas_quote(session_stack) + ")"
   }