reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
authorwenzelm
Mon, 25 Feb 2013 11:07:02 +0100
changeset 5240717d30843fc3b
parent 52406 54725c4acdd0
child 52408 e8d2ecf6aaac
reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Pure.thy
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Feb 25 10:50:52 2013 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Feb 25 11:07:02 2013 +0100
     1.3 @@ -270,6 +270,7 @@
     1.4      "kill"
     1.5      "kill_thy"
     1.6      "linear_undo"
     1.7 +    "pretty_setmargin"
     1.8      "quit"
     1.9      "remove_thy"
    1.10      "undo"
    1.11 @@ -289,7 +290,6 @@
    1.12      "help"
    1.13      "locale_deps"
    1.14      "pr"
    1.15 -    "pretty_setmargin"
    1.16      "prf"
    1.17      "print_abbrevs"
    1.18      "print_antiquotations"
     2.1 --- a/etc/isar-keywords.el	Mon Feb 25 10:50:52 2013 +0100
     2.2 +++ b/etc/isar-keywords.el	Mon Feb 25 11:07:02 2013 +0100
     2.3 @@ -367,6 +367,7 @@
     2.4      "kill"
     2.5      "kill_thy"
     2.6      "linear_undo"
     2.7 +    "pretty_setmargin"
     2.8      "quit"
     2.9      "remove_thy"
    2.10      "undo"
    2.11 @@ -392,7 +393,6 @@
    2.12      "locale_deps"
    2.13      "nitpick"
    2.14      "pr"
    2.15 -    "pretty_setmargin"
    2.16      "prf"
    2.17      "print_abbrevs"
    2.18      "print_antiquotations"
     3.1 --- a/src/Pure/Pure.thy	Mon Feb 25 10:50:52 2013 +0100
     3.2 +++ b/src/Pure/Pure.thy	Mon Feb 25 11:07:02 2013 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4    and "finally" "ultimately" :: prf_chain % "proof"
     3.5    and "back" :: prf_script % "proof"
     3.6    and "Isabelle.command" :: control
     3.7 -  and "pretty_setmargin" "help" "print_commands" "print_configs"
     3.8 +  and "help" "print_commands" "print_configs"
     3.9      "print_context" "print_theory" "print_syntax" "print_abbrevs"
    3.10      "print_theorems" "print_locales" "print_classes" "print_locale"
    3.11      "print_interps" "print_dependencies" "print_attributes"
    3.12 @@ -88,7 +88,7 @@
    3.13    and "pwd" :: diag
    3.14    and "use_thy" "remove_thy" "kill_thy" :: control
    3.15    and "display_drafts" "print_drafts" "pr" :: diag
    3.16 -  and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    3.17 +  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    3.18    and "welcome" :: diag
    3.19    and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    3.20    and "end" :: thy_end % "theory"