# HG changeset patch
# User aspinall
# Date 1169481122 -3600
# Node ID a586b0af857e09451428bd031f8c69c5368b0783
# Parent  63dbc68eb5274ca0665b8d20475a33af7d71fdd1
Expose currently open file

diff -r 63dbc68eb527 -r a586b0af857e src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 22 16:51:29 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 22 16:52:02 2007 +0100
@@ -17,8 +17,9 @@
   (* Yet more message functions... *)
   val nonfatal_error : string -> unit     (* recoverable error *)
   val log_msg : string -> unit	          (* for internal log messages *)
+  val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit
 
-  val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit
+  val get_currently_open_file : unit -> Path.T option  (* interface focus *)
 end
 
 structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
@@ -696,6 +697,8 @@
 
 val currently_open_file = ref (NONE : pgipurl option)
 
+fun get_currently_open_file () = ! currently_open_file;
+
 fun askguise vs =
     (* The "guise" is the PGIP abstraction of the prover's state.
        The <informguise> message is merely used for consistency checking. *)