# HG changeset patch
# User Simon Wimmer <wimmers@in.tum.de>
# Date 1710189078 -3600
# Node ID 8f0ff2847ba8ba26a855a0884bb11cb55bfcf8e3
# Parent  c73a36081b1c5a6448c80a1bbffc91a399bd2522
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text

diff -r c73a36081b1c -r 8f0ff2847ba8 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Fri Mar 15 17:57:03 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:31:18 2024 +0100
@@ -67,10 +67,10 @@
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
-    val prefix_sep = "\n" ^ prefix ^ "    and ";
+    val prefix_sep = "\n" ^ prefix ^ "  and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val assumes_s = if null assms then NONE
-      else SOME (prefix ^ "  assume " ^ space_implode prefix_sep
+      else SOME (prefix ^ "assume " ^ space_implode prefix_sep
         (map (print_term ctxt') assms));
     val fixes_s = if null fixes then NONE
       else SOME (prefix ^ "fix " ^ space_implode prefix_sep
@@ -123,7 +123,7 @@
       if is_none some_method_ref then ["  .."]
       else ["  by" ^ method_text]
       else print ctxt_print method_text clauses;
-    val message = Active.sendback_markup_properties [] (cat_lines lines);
+    val message = Active.sendback_markup_command (cat_lines lines);
   in
     (state |> tap (fn _ => Output.information message))
   end