src/Pure/PIDE/command.ML
changeset 63474 f66e3c3b0fb1
parent 62924 ce47945ce4fb
child 63475 31016a88197b
--- a/src/Pure/PIDE/command.ML	Wed Jul 13 14:28:15 2016 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 13 15:19:16 2016 +0200
@@ -214,12 +214,28 @@
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
+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 => ())
+        else ()
+      end
+  | NONE => ());
+
+
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
     val _ = Thread_Attributes.expose_interrupt ();
 
     val st = reset_state keywords tr state;
 
+    val _ = command_indent tr st;
     val _ = status tr Markup.running;
     val (errs1, result) = run keywords true tr st;
     val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');