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 =