Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/proof_general.ML
changeset 18587 d4dcdfd764a0
parent 18560 6b4570eb22d2
child 18678 dd0c569fa43d 
--- 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
isabelle