# HG changeset patch
# User aspinall
# Date 1121246889 -7200
# Node ID 0c6f5fe3067605de31aab4ff8bde3772b6fdf414
# Parent  b6b6e2faaa41ed92e2a909444725f488fb6de0a0
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc

diff -r b6b6e2faaa41 -r 0c6f5fe30676 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Jul 13 11:16:34 2005 +0200
+++ b/src/Pure/proof_general.ML	Wed Jul 13 11:28:09 2005 +0200
@@ -316,17 +316,15 @@
 
 fun tell_file_loaded path =
   if pgip () then
-    issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
-      [thyname_attr        (XML.text (File.platform_path path)),
-       localfile_url_attr  (XML.text (File.platform_path path))]
+    issue_pgipe "informfileloaded"
+      [localfile_url_attr  (XML.text (File.platform_path path))]
   else
     emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
 
 fun tell_file_retracted path =
   if pgip() then
-    issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
-      [thyname_attr        (XML.text (File.platform_path path)),
-       localfile_url_attr  (XML.text (File.platform_path path))]
+    issue_pgipe "informfileretracted"
+      [localfile_url_attr  (XML.text (File.platform_path path))]
   else
     emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
 
@@ -900,17 +898,21 @@
             (empty "openblock")
         end
 
-    fun xmls_of_qed (name,markup) = (case name of
-      "sorry"         => markup "giveupgoal"
-    | "oops"          => markup "postponegoal"
-    | "done"          => markup "closegoal"
-    | "by"            => markup "closegoal"  (* nested or toplevel *)
-    | "qed"           => markup "closegoal"  (* nested or toplevel *)
-    | "."             => markup "closegoal"  (* nested or toplevel *)
-    | ".."            => markup "closegoal"  (* nested or toplevel *)
-    | other => (* default to closegoal: may be wrong for extns *)
-      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal"))
-        @ (empty "closeblock")
+    fun xmls_of_qed (name,markup) = 
+	let val qedmarkup  = 
+		(case name of
+		     "sorry" => markup "postponegoal"
+		   | "oops"  => markup "giveupgoal"
+		   | "done"  => markup "closegoal" 
+		   | "by"    => markup "closegoal"  (* nested or toplevel *)
+		   | "qed"   => markup "closegoal"  (* nested or toplevel *)
+		   | "."     => markup "closegoal"  (* nested or toplevel *)
+		   | ".."    => markup "closegoal"  (* nested or toplevel *)
+		   | other => (* default to closegoal: may be wrong for extns *)
+				  (parse_warning 
+				       ("Unrecognized qed command: " ^ quote other); 
+				       markup "closegoal"))
+	in qedmarkup @ (empty "closeblock") end
 
     fun xmls_of_kind kind (name,toks,str) =
     let val markup = markup_text str in