changeset 76804 | 3e8340fcaa16 |
parent 74887 | 56247fdb8bbb |
child 77908 | a6bd716a6124 |
--- a/src/Pure/Isar/method.ML Wed Dec 28 16:02:12 2022 +0100 +++ b/src/Pure/Isar/method.ML Wed Dec 28 16:13:08 2022 +0100 @@ -667,7 +667,7 @@ (keyword_positions text); fun report text_range = - if Context_Position.pide_reports () + if Context_Position.reports_enabled0 () then Position.reports (reports_of text_range) else (); end;