# HG changeset patch
# User wenzelm
# Date 1259012154 -3600
# Node ID 04c560b4ebc140cd6fe54629cd1a63ba38ac7f82
# Parent  caab5399bb2dd5bb86e4a909c225b37e05568c6f
added command 'ProofGeneral.pr' for PG 4.0;

diff -r caab5399bb2d -r 04c560b4ebc1 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Nov 23 21:56:07 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Nov 23 22:35:54 2009 +0100
@@ -190,6 +190,12 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+fun prP () =
+  OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.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)" K.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
@@ -219,7 +225,8 @@
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
 
 fun init_outer_syntax () = List.app (fn f => f ())
-  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
+  [prP, undoP, restartP, kill_proofP, inform_file_processedP,
+    inform_file_retractedP, process_pgipP];
 
 end;