src/Pure/Thy/sessions.scala
changeset 75920 27bf2533f4a4
parent 75917 20b918404aa3
child 75921 423021c98500
--- a/src/Pure/Thy/sessions.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -364,8 +364,11 @@
     errors: List[String] = Nil,
     infos: List[Info] = Nil
   ) {
-    def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
     def session: String = base.session_name
+
+    def check_errors: Base_Info =
+      if (errors.isEmpty) this
+      else error(cat_lines(errors))
   }
 
   def base_info0(session: String): Base_Info =