src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 50277 e0a4d8404c76
parent 50276 1db687c43663
child 50410 6ab3fadf43af
equal deleted inserted replaced
50276:1db687c43663 50277:e0a4d8404c76
   700        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
   700        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
   701           |>> chain_direct_proof
   701           |>> chain_direct_proof
   702           |>> kill_useless_labels_in_proof
   702           |>> kill_useless_labels_in_proof
   703           |>> relabel_proof
   703           |>> relabel_proof
   704           |>> not (null params) ? cons (Fix params)
   704           |>> not (null params) ? cons (Fix params)
   705         val num_steps = metis_steps_total isar_proof
       
   706         val isar_text =
   705         val isar_text =
   707           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
   706           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
   708                            isar_proof
   707                            isar_proof
   709       in
   708       in
   710         case isar_text of
   709         case isar_text of
   713             "\nNo structured proof available (proof too short)."
   712             "\nNo structured proof available (proof too short)."
   714           else
   713           else
   715             ""
   714             ""
   716         | _ =>
   715         | _ =>
   717           let 
   716           let 
   718             val preplay_msg = if preplay_fail
   717             val msg = 
   719               then "may fail"
   718               (if preplay then 
   720               else string_from_ext_time ext_time
   719                 [if preplay_fail 
   721             val shrank_without_preplay_msg =
   720                  then "may fail" 
   722               "may fail - shrank proof, but did not preplay"
   721                  else string_from_ext_time ext_time]
   723             in
   722                else [])
   724               "\n\nStructured proof"
   723               @ 
   725                 ^ (if verbose then
   724                (if verbose then
   726                     " (" ^ string_of_int num_steps 
   725                   [let val num_steps = metis_steps_total isar_proof
   727                          ^ " metis step" ^ plural_s num_steps
   726                    in string_of_int num_steps ^ plural_s num_steps end]
   728                          |> (if preplay then 
   727                 else [])
   729                                suffix (", " ^ preplay_msg)
   728           in
   730                              else if isar_shrink > 1.0 then
   729             "\n\nStructured proof "
   731                                suffix (", " ^ shrank_without_preplay_msg)
   730               ^ (commas msg |> not (null msg) ? enclose "(" ")")
   732                              else I)
   731               ^ ":\n" ^ Markup.markup Markup.sendback isar_text
   733                          |> suffix ")"
   732           end
   734                    else if preplay then
       
   735                      " (" ^ preplay_msg ^ ")"
       
   736                    else if isar_shrink > 1.0 then
       
   737                      " (" ^ shrank_without_preplay_msg ^ ")"
       
   738                    else
       
   739                      "") 
       
   740                 ^ ":\n" ^ Markup.markup Markup.sendback isar_text
       
   741             end
       
   742       end
   733       end
   743     val isar_proof =
   734     val isar_proof =
   744       if debug then
   735       if debug then
   745         isar_proof_of ()
   736         isar_proof_of ()
   746       else case try isar_proof_of () of
   737       else case try isar_proof_of () of