--- 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. *)