# HG changeset patch
# User wenzelm
# Date 1361786822 -3600
# Node ID 17d30843fc3b19b88c25cb49f569ed0bb3171fd0
# Parent  54725c4acdd01f00334ee7055ed4f13aae073150
reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;

diff -r 54725c4acdd0 -r 17d30843fc3b etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Feb 25 10:50:52 2013 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Feb 25 11:07:02 2013 +0100
@@ -270,6 +270,7 @@
     "kill"
     "kill_thy"
     "linear_undo"
+    "pretty_setmargin"
     "quit"
     "remove_thy"
     "undo"
@@ -289,7 +290,6 @@
     "help"
     "locale_deps"
     "pr"
-    "pretty_setmargin"
     "prf"
     "print_abbrevs"
     "print_antiquotations"
diff -r 54725c4acdd0 -r 17d30843fc3b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Feb 25 10:50:52 2013 +0100
+++ b/etc/isar-keywords.el	Mon Feb 25 11:07:02 2013 +0100
@@ -367,6 +367,7 @@
     "kill"
     "kill_thy"
     "linear_undo"
+    "pretty_setmargin"
     "quit"
     "remove_thy"
     "undo"
@@ -392,7 +393,6 @@
     "locale_deps"
     "nitpick"
     "pr"
-    "pretty_setmargin"
     "prf"
     "print_abbrevs"
     "print_antiquotations"
diff -r 54725c4acdd0 -r 17d30843fc3b src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Feb 25 10:50:52 2013 +0100
+++ b/src/Pure/Pure.thy	Mon Feb 25 11:07:02 2013 +0100
@@ -75,7 +75,7 @@
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
   and "Isabelle.command" :: control
-  and "pretty_setmargin" "help" "print_commands" "print_configs"
+  and "help" "print_commands" "print_configs"
     "print_context" "print_theory" "print_syntax" "print_abbrevs"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
@@ -88,7 +88,7 @@
   and "pwd" :: diag
   and "use_thy" "remove_thy" "kill_thy" :: control
   and "display_drafts" "print_drafts" "pr" :: diag
-  and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  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"