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 36953 2af1ad9aa1a3
parent 36950 75b8f26f2f07
child 37216 3165bc303f66 
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 23:32:15 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat May 15 23:40:00 2010 +0200
@@ -189,36 +189,36 @@
 (* additional outer syntax for Isar *)
 
 fun prP () =
-  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
+  Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
     (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))));
 
 fun undoP () = (*undo without output -- historical*)
-  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 fun restartP () =
-  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 fun kill_proofP () =
-  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 fun inform_file_processedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
     (Parse.name >> (fn file =>
       Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
 
 fun inform_file_retractedP () =
-  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
     (Parse.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
 
 fun process_pgipP () =
-  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+  Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
     (Parse.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
isabelle