src/Pure/Isar/proof_context.ML
changeset 73872 b0ea03e837b1
parent 72137 f8b0271cc744
child 73947 9267a04aabe6
equal deleted inserted replaced
73871:e768759ce6c5 73872:b0ea03e837b1
  1543       | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
  1543       | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
  1544 
  1544 
  1545     fun is_case x t =
  1545     fun is_case x t =
  1546       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
  1546       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
  1547 
  1547 
  1548     fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
  1548     fun indentation depth = prefix (Symbol.spaces (2 * depth));
  1549       let
  1549 
  1550         val concl =
  1550     fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) =
  1551           if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
  1551           let
  1552           then Rule_Cases.case_conclN else Auto_Bind.thesisN;
  1552             val indent = indentation depth;
  1553       in
  1553             val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes));
  1554         cat_lines
  1554             val tail =
  1555           ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
  1555               if null cases then
  1556            "  then show ?" ^ concl ^ " sorry"]
  1556                 let val concl =
  1557       end;
  1557                   if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
       
  1558                   then Rule_Cases.case_conclN else Auto_Bind.thesisN
       
  1559                 in indent ("then show ?" ^ concl ^ " sorry") end
       
  1560               else print_proofs depth cases;
       
  1561           in head ^ "\n" ^ tail end
       
  1562     and print_proofs 0 [] = ""
       
  1563       | print_proofs depth cases =
       
  1564           let
       
  1565             val indent = indentation depth;
       
  1566             val body = map (print_proof (depth + 1)) cases |> separate (indent "next")
       
  1567           in
       
  1568             if depth = 0 then body @ [indent "qed"]
       
  1569             else if length cases = 1 then body
       
  1570             else indent "{" :: body @ [indent "}"]
       
  1571           end |> cat_lines;
  1558   in
  1572   in
  1559     (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
  1573     (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of
  1560       [] => ""
  1574       "" => ""
  1561     | proofs =>
  1575     | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s)
  1562         "Proof outline with cases:\n" ^
       
  1563         Active.sendback_markup_command (space_implode "\nnext\n" proofs ^ "\nqed"))
       
  1564   end;
  1576   end;
  1565 
  1577 
  1566 
  1578 
  1567 (* core context *)
  1579 (* core context *)
  1568 
  1580