# HG changeset patch
# User wenzelm
# Date 1610112598 -3600
# Node ID e700ede0038fd813715943b2ad6d7dc344e32b91
# Parent  84cde7fc4b86cf84be810f815d21ddece9486279
tuned;

diff -r 84cde7fc4b86 -r e700ede0038f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 08 14:05:46 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 14:29:58 2021 +0100
@@ -234,27 +234,26 @@
 fun check_span_comments ctxt span tr =
   Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
 
-fun report tr m =
-  Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
-
-fun status tr m =
-  Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
-
 fun command_indent tr st =
   (case try Toplevel.proof_of st of
     SOME prf =>
       let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in
         if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then
-          (case try Proof.goal prf of
-            SOME {goal, ...} =>
-              let val n = Thm.nprems_of goal
-              in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end
-          | NONE => ())
+          (case try (Thm.nprems_of o #goal o Proof.goal) prf of
+            NONE => ()
+          | SOME 0 => ()
+          | SOME n =>
+              let
+                val m = Markup.command_indent (n - 1);
+              in Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) () end)
         else ()
       end
   | NONE => ());
 
 
+fun status tr m =
+  Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
+
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
     val _ = Thread_Attributes.expose_interrupt ();