# HG changeset patch
# User wenzelm
# Date 1610113338 -3600
# Node ID ccbefeb3a50d27c60868611b2ec794e3f83c89d7
# Parent  8a20737e4ebff5a3cab89c568a1e0afbbc1500bc
tuned;

diff -r 8a20737e4ebf -r ccbefeb3a50d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 08 14:40:04 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 14:42:18 2021 +0100
@@ -234,7 +234,7 @@
 fun check_span_comments ctxt span tr =
   Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
 
-fun command_indent tr st =
+fun report_indent tr st =
   (case try Toplevel.proof_of st of
     SOME prf =>
       let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in
@@ -250,7 +250,6 @@
       end
   | NONE => ());
 
-
 fun status tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
 
@@ -260,7 +259,7 @@
 
     val st = reset_state keywords tr state;
 
-    val _ = command_indent tr st;
+    val _ = report_indent tr st;
     val _ = status tr Markup.running;
     val (errs1, result) = run keywords true tr st;
     val errs2 =