Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
inform_file_processed: Toplevel.init_empty;
authorwenzelm
Sat, 30 Dec 2006 12:33:29 +0100
changeset 21959 b50182aff75f
parent 21958 9dfd1ca4c0a0
child 21960 0574f192b78a
inform_file_processed: Toplevel.init_empty;
src/Pure/ProofGeneral/proof_general_emacs.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/proof_general_pgip.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 12:33:28 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 12:33:29 2006 +0100
@@ -177,7 +177,6 @@
 
 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
-val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
 
 fun proper_inform_file_processed file state =
   let val name = thy_name file in
@@ -254,9 +253,9 @@
 val inform_file_processedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.keep (vacuous_inform_file_processed file) o
+      Toplevel.init_empty (vacuous_inform_file_processed file) o
       Toplevel.kill o
-      Toplevel.keep (proper_inform_file_processed file)));
+      Toplevel.init_empty (proper_inform_file_processed file)));
 
 val inform_file_retractedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 12:33:28 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 12:33:29 2006 +0100
@@ -944,9 +944,9 @@
 val inform_file_processedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.keep (vacuous_inform_file_processed file) o
+      Toplevel.init_empty (vacuous_inform_file_processed file) o
       Toplevel.kill o
-      Toplevel.keep (proper_inform_file_processed file)));
+      Toplevel.init_empty (proper_inform_file_processed file)));
 
 val inform_file_retractedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
isabelle