# HG changeset patch
# User wenzelm
# Date 1619969929 -7200
# Node ID b0ea03e837b1289ca22a44ca886a042dc297860b
# Parent  e768759ce6c59402f82cf1f0f7b775bd01ae6427
support nested cases;

diff -r e768759ce6c5 -r b0ea03e837b1 NEWS
--- a/NEWS	Sun May 02 15:56:58 2021 +0200
+++ b/NEWS	Sun May 02 17:38:49 2021 +0200
@@ -27,6 +27,11 @@
 Isabelle/jEdit.
 
 
+*** Isabelle/jEdit Prover IDE ***
+
+* More robust 'proof' outline for method "induct": support nested cases.
+
+
 *** Document preparation ***
 
 * Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
diff -r e768759ce6c5 -r b0ea03e837b1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun May 02 15:56:58 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun May 02 17:38:49 2021 +0200
@@ -1545,22 +1545,34 @@
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
 
-    fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
-      let
-        val concl =
-          if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
-          then Rule_Cases.case_conclN else Auto_Bind.thesisN;
-      in
-        cat_lines
-          ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
-           "  then show ?" ^ concl ^ " sorry"]
-      end;
+    fun indentation depth = prefix (Symbol.spaces (2 * depth));
+
+    fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) =
+          let
+            val indent = indentation depth;
+            val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes));
+            val tail =
+              if null cases then
+                let val concl =
+                  if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
+                  then Rule_Cases.case_conclN else Auto_Bind.thesisN
+                in indent ("then show ?" ^ concl ^ " sorry") end
+              else print_proofs depth cases;
+          in head ^ "\n" ^ tail end
+    and print_proofs 0 [] = ""
+      | print_proofs depth cases =
+          let
+            val indent = indentation depth;
+            val body = map (print_proof (depth + 1)) cases |> separate (indent "next")
+          in
+            if depth = 0 then body @ [indent "qed"]
+            else if length cases = 1 then body
+            else indent "{" :: body @ [indent "}"]
+          end |> cat_lines;
   in
-    (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
-      [] => ""
-    | proofs =>
-        "Proof outline with cases:\n" ^
-        Active.sendback_markup_command (space_implode "\nnext\n" proofs ^ "\nqed"))
+    (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of
+      "" => ""
+    | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s)
   end;