src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 24867 e5b55d7be9bb
parent 24712 64ed05609568
child 24873 9de439f51e3c
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -231,36 +231,36 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val undoP = (*undo without output*)
     1.8 +fun undoP () = (*undo without output*)
     1.9    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
    1.10      (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
    1.11  
    1.12 -val restartP =
    1.13 +fun restartP () =
    1.14    OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
    1.15      (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
    1.16  
    1.17 -val kill_proofP =
    1.18 +fun kill_proofP () =
    1.19    OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
    1.20      (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
    1.21  
    1.22 -val inform_file_processedP =
    1.23 +fun inform_file_processedP () =
    1.24    OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
    1.25      (P.name >> (fn file => Toplevel.no_timing o
    1.26        Toplevel.init_empty (vacuous_inform_file_processed file) o
    1.27        Toplevel.kill o
    1.28        Toplevel.init_empty (proper_inform_file_processed file)));
    1.29  
    1.30 -val inform_file_retractedP =
    1.31 +fun inform_file_retractedP () =
    1.32    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
    1.33      (P.name >> (Toplevel.no_timing oo
    1.34        (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
    1.35  
    1.36 -val process_pgipP =
    1.37 +fun process_pgipP () =
    1.38    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
    1.39      (P.text >> (Toplevel.no_timing oo
    1.40        (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
    1.41  
    1.42 -fun init_outer_syntax () = OuterSyntax.add_parsers
    1.43 +fun init_outer_syntax () = List.app (fn f => f ())
    1.44   [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
    1.45  
    1.46  end;