back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
authorwenzelm
Mon Jun 24 17:17:17 2013 +0200 (2013-06-24)
changeset 524387b5a5116f3af
parent 52437 c88354589b43
child 52439 4cf3f6153eb8
back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Jun 24 17:03:53 2013 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Jun 24 17:17:17 2013 +0200
     1.3 @@ -269,7 +269,6 @@
     1.4      "kill"
     1.5      "kill_thy"
     1.6      "linear_undo"
     1.7 -    "pr"
     1.8      "pretty_setmargin"
     1.9      "quit"
    1.10      "remove_thy"
    1.11 @@ -288,6 +287,7 @@
    1.12      "header"
    1.13      "help"
    1.14      "locale_deps"
    1.15 +    "pr"
    1.16      "prf"
    1.17      "print_abbrevs"
    1.18      "print_antiquotations"
     2.1 --- a/etc/isar-keywords.el	Mon Jun 24 17:03:53 2013 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Jun 24 17:17:17 2013 +0200
     2.3 @@ -375,7 +375,6 @@
     2.4      "kill"
     2.5      "kill_thy"
     2.6      "linear_undo"
     2.7 -    "pr"
     2.8      "pretty_setmargin"
     2.9      "quit"
    2.10      "remove_thy"
    2.11 @@ -399,6 +398,7 @@
    2.12      "help"
    2.13      "locale_deps"
    2.14      "nitpick"
    2.15 +    "pr"
    2.16      "prf"
    2.17      "print_abbrevs"
    2.18      "print_antiquotations"
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jun 24 17:03:53 2013 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 24 17:17:17 2013 +0200
     3.3 @@ -980,7 +980,8 @@
     3.4    Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
     3.5      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
     3.6        Toplevel.keep (fn state =>
     3.7 -       (case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
     3.8 +       (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
     3.9 +        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
    3.10          Toplevel.quiet := false;
    3.11          Print_Mode.with_modes modes (Toplevel.print_state true) state))));
    3.12  
     4.1 --- a/src/Pure/Pure.thy	Mon Jun 24 17:03:53 2013 +0200
     4.2 +++ b/src/Pure/Pure.thy	Mon Jun 24 17:17:17 2013 +0200
     4.3 @@ -86,8 +86,8 @@
     4.4    and "cd" :: control
     4.5    and "pwd" :: diag
     4.6    and "use_thy" "remove_thy" "kill_thy" :: control
     4.7 -  and "display_drafts" "print_drafts" "print_state" :: diag
     4.8 -  and "pr" "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
     4.9 +  and "display_drafts" "print_drafts" "print_state" "pr" :: diag
    4.10 +  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    4.11    and "welcome" :: diag
    4.12    and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    4.13    and "end" :: thy_end % "theory"