inform_file_processed: Toplevel.init_empty;
authorwenzelm
Sat Dec 30 12:33:29 2006 +0100 (2006-12-30)
changeset 21959b50182aff75f
parent 21958 9dfd1ca4c0a0
child 21960 0574f192b78a
inform_file_processed: Toplevel.init_empty;
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 12:33:28 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 12:33:29 2006 +0100
     1.3 @@ -177,7 +177,6 @@
     1.4  
     1.5  val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
     1.6  val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
     1.7 -val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
     1.8  
     1.9  fun proper_inform_file_processed file state =
    1.10    let val name = thy_name file in
    1.11 @@ -254,9 +253,9 @@
    1.12  val inform_file_processedP =
    1.13    OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
    1.14      (P.name >> (fn file => Toplevel.no_timing o
    1.15 -      Toplevel.keep (vacuous_inform_file_processed file) o
    1.16 +      Toplevel.init_empty (vacuous_inform_file_processed file) o
    1.17        Toplevel.kill o
    1.18 -      Toplevel.keep (proper_inform_file_processed file)));
    1.19 +      Toplevel.init_empty (proper_inform_file_processed file)));
    1.20  
    1.21  val inform_file_retractedP =
    1.22    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 12:33:28 2006 +0100
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 30 12:33:29 2006 +0100
     2.3 @@ -944,9 +944,9 @@
     2.4  val inform_file_processedP =
     2.5    OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     2.6      (P.name >> (fn file => Toplevel.no_timing o
     2.7 -      Toplevel.keep (vacuous_inform_file_processed file) o
     2.8 +      Toplevel.init_empty (vacuous_inform_file_processed file) o
     2.9        Toplevel.kill o
    2.10 -      Toplevel.keep (proper_inform_file_processed file)));
    2.11 +      Toplevel.init_empty (proper_inform_file_processed file)));
    2.12  
    2.13  val inform_file_retractedP =
    2.14    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control