# HG changeset patch # User wenzelm # Date 1136496598 -3600 # Node ID d4dcdfd764a0a3c7076ad2b621faa5fafc08f0ef # Parent 588e802896589bcaf40258023c3b5be4682ec57b Toplevel.proof_position_of; diff -r 588e80289658 -r d4dcdfd764a0 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Jan 05 22:29:57 2006 +0100 +++ b/src/Pure/proof_general.ML Thu Jan 05 22:29:58 2006 +0100 @@ -1196,9 +1196,7 @@ current_working_dir := SOME dir) end - val topnode = Toplevel.node_of o Toplevel.get_state - fun topproofpos () = (case topnode() of Toplevel.Proof (h, _) => SOME(ProofHistory.position h) - | _ => NONE) handle Toplevel.UNDEF => NONE + fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); in fun process_pgip_element pgipxml = (case pgipxml of