Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 46961 5c6955f487e5
parent 46737 09ab89658a5d
child 48646 91281e9472d8 
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -189,31 +189,31 @@
 (* additional outer syntax for Isar *)
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
+  Outer_Syntax.improper_command ("ProofGeneral.pr", Keyword.diag) "print state (internal)"
     (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
       if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
       else (Toplevel.quiet := false; Toplevel.print_state true state))));
 
 val _ = (*undo without output -- historical*)
-  Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.undo", Keyword.control) "(internal)"
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.restart", Keyword.control) "(internal)"
     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.kill_proof", Keyword.control) "(internal)"
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.inform_file_processed", Keyword.control) "(internal)"
     (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 val _ =
-  Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+  Outer_Syntax.improper_command ("ProofGeneral.inform_file_retracted", Keyword.control) "(internal)"
     (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
isabelle