tuned;
authorwenzelm
Fri, 08 Jan 2021 14:42:18 +0100
changeset 73099 ccbefeb3a50d
parent 73098 8a20737e4ebf
child 73100 693a39f2cddc
tuned;
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 =