equal
deleted
inserted
replaced
301 |
301 |
302 |
302 |
303 (* diagnostic ML evaluation *) |
303 (* diagnostic ML evaluation *) |
304 |
304 |
305 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => |
305 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state => |
306 (ML_Context.eval_in (try Toplevel.generic_theory_of state) verbose pos txt)); |
306 (ML_Context.eval_in |
|
307 (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt)); |
307 |
308 |
308 |
309 |
309 (* current working directory *) |
310 (* current working directory *) |
310 |
311 |
311 fun cd path = Toplevel.imperative (fn () => (File.cd path)); |
312 fun cd path = Toplevel.imperative (fn () => (File.cd path)); |