equal
deleted
inserted
replaced
135 (outcome_code, |
135 (outcome_code, |
136 state |
136 state |
137 |> outcome_code = someN |
137 |> outcome_code = someN |
138 ? Proof.goal_message (fn () => |
138 ? Proof.goal_message (fn () => |
139 [Pretty.str "", |
139 [Pretty.str "", |
140 Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))] |
140 Pretty.mark Markup.intensify (Pretty.str (message ()))] |
141 |> Pretty.chunks)) |
141 |> Pretty.chunks)) |
142 end |
142 end |
143 else if blocking then |
143 else if blocking then |
144 let |
144 let |
145 val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () |
145 val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () |