src/Tools/solve_direct.ML
changeset 49358 0fa351b1bd14
parent 46961 5c6955f487e5
child 50201 c26369c9eda6
equal deleted inserted replaced
49357:34ac36642a31 49358:0fa351b1bd14
    87           state |>
    87           state |>
    88             (if mode = Auto_Try then
    88             (if mode = Auto_Try then
    89                Proof.goal_message
    89                Proof.goal_message
    90                  (fn () =>
    90                  (fn () =>
    91                    Pretty.chunks
    91                    Pretty.chunks
    92                     [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
    92                     [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
    93              else
    93              else
    94                tap (fn _ =>
    94                tap (fn _ =>
    95                  Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    95                  Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    96     | SOME NONE =>
    96     | SOME NONE =>
    97         (if mode = Normal then Output.urgent_message "No proof found."
    97         (if mode = Normal then Output.urgent_message "No proof found."