equal
deleted
inserted
replaced
1332 in (Future.map fst result_ctxt, state') end; |
1332 in (Future.map fst result_ctxt, state') end; |
1333 |
1333 |
1334 end; |
1334 end; |
1335 |
1335 |
1336 |
1336 |
1337 (* terminal proofs *) (* FIXME avoid toplevel imitation -- include in PIDE/document *) |
1337 (* terminal proofs *) |
1338 |
1338 |
1339 local |
1339 local |
1340 |
1340 |
1341 fun future_terminal_proof proof1 proof2 done state = |
1341 fun future_terminal_proof proof1 proof2 done state = |
1342 if Future.proofs_enabled 3 andalso |
1342 if Future.proofs_enabled 3 andalso |