changeset 69892 | f752f3993db8 |
parent 69891 | def3ec9cdb7e |
child 70662 | 0f9a4e8ee1ab |
--- a/src/Pure/PIDE/command.ML Sun Mar 10 21:12:29 2019 +0100 +++ b/src/Pure/PIDE/command.ML Sun Mar 10 21:31:28 2019 +0100 @@ -262,10 +262,7 @@ val errs2 = (case result of NONE => [] - | SOME st' => - (case try Toplevel.presentation_context st' of - NONE => [] - | SOME ctxt' => check_span_comments ctxt' span tr)); + | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in