src/Pure/PIDE/command.ML
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