back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;

--- a/etc/isar-keywords-ZF.el	Mon Jun 24 17:03:53 2013 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Jun 24 17:17:17 2013 +0200
@@ -269,7 +269,6 @@
     "kill"
     "kill_thy"
     "linear_undo"
-    "pr"
     "pretty_setmargin"
     "quit"
     "remove_thy"
@@ -288,6 +287,7 @@
     "header"
     "help"
     "locale_deps"
+    "pr"
     "prf"
     "print_abbrevs"
     "print_antiquotations"

--- a/etc/isar-keywords.el	Mon Jun 24 17:03:53 2013 +0200
+++ b/etc/isar-keywords.el	Mon Jun 24 17:17:17 2013 +0200
@@ -375,7 +375,6 @@
     "kill"
     "kill_thy"
     "linear_undo"
-    "pr"
     "pretty_setmargin"
     "quit"
     "remove_thy"
@@ -399,6 +398,7 @@
     "help"
     "locale_deps"
     "nitpick"
+    "pr"
     "prf"
     "print_abbrevs"
     "print_antiquotations"

--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 24 17:03:53 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 24 17:17:17 2013 +0200
@@ -980,7 +980,8 @@
   Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.keep (fn state =>
-       (case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
+       (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
+        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 

--- a/src/Pure/Pure.thy	Mon Jun 24 17:03:53 2013 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 24 17:17:17 2013 +0200
@@ -86,8 +86,8 @@
   and "cd" :: control
   and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
-  and "display_drafts" "print_drafts" "print_state" :: diag
-  and "pr" "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "display_drafts" "print_drafts" "print_state" "pr" :: diag
+  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
   and "welcome" :: diag
   and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
   and "end" :: thy_end % "theory"