1.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 10 09:16:44 2020 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 10 14:38:32 2020 +0100
     1.3 @@ -395,6 +395,16 @@
     1.4        else [];
     1.5  
     1.6      val position_markup = Position.markup (Position.thread_data ()) Markup.position;
     1.7 +(*//---------------------------- test code: NO @{print} available ------------------------\\* )
     1.8 +    val part1 = [Pretty.block
     1.9 +      [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]]
    1.10 +    val part3 = (if verbose orelse mode = Forward then
    1.11 +       pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state))
    1.12 +     else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts)
    1.13 +     else prt_goal (try find_goal state))
    1.14 +(*------------------------------ test code: NO @{print} available --------------------------*)
    1.15 +    val _ = @{print} {a = "pretty_state:", part1 = part1, part3 = part3}
    1.16 +( *\\---------------------------- test code: NO @{print} available ------------------------//*)
    1.17    in
    1.18      [Pretty.block
    1.19        [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @