proper diagnostic command 'print_state';
authorwenzelm
Sun Jun 23 21:23:36 2013 +0200 (2013-06-23)
changeset 52430289e36c2870a
parent 52429 921f22c8890e
child 52431 7fa1245f50df
proper diagnostic command 'print_state';
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarRef/Inner_Syntax.thy
src/Doc/IsarRef/Quick_Reference.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sun Jun 23 21:15:42 2013 +0200
     1.2 +++ b/NEWS	Sun Jun 23 21:23:36 2013 +0200
     1.3 @@ -32,6 +32,10 @@
     1.4  * Updated and extended "isar-ref" and "implementation" manual,
     1.5  eliminated old "ref" manual.
     1.6  
     1.7 +* Proper diagnostic command 'print_state'.  Old 'pr' (with its
     1.8 +implicit change of some global references) is retained for now as
     1.9 +control command, e.g. for ProofGeneral 3.7.x.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/etc/isar-keywords-ZF.el	Sun Jun 23 21:15:42 2013 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Sun Jun 23 21:23:36 2013 +0200
     2.3 @@ -143,6 +143,7 @@
     2.4      "print_options"
     2.5      "print_rules"
     2.6      "print_simpset"
     2.7 +    "print_state"
     2.8      "print_statement"
     2.9      "print_syntax"
    2.10      "print_tcset"
    2.11 @@ -267,6 +268,7 @@
    2.12      "kill"
    2.13      "kill_thy"
    2.14      "linear_undo"
    2.15 +    "pr"
    2.16      "pretty_setmargin"
    2.17      "quit"
    2.18      "remove_thy"
    2.19 @@ -286,7 +288,6 @@
    2.20      "header"
    2.21      "help"
    2.22      "locale_deps"
    2.23 -    "pr"
    2.24      "prf"
    2.25      "print_abbrevs"
    2.26      "print_antiquotations"
    2.27 @@ -311,6 +312,7 @@
    2.28      "print_options"
    2.29      "print_rules"
    2.30      "print_simpset"
    2.31 +    "print_state"
    2.32      "print_statement"
    2.33      "print_syntax"
    2.34      "print_tcset"
     3.1 --- a/etc/isar-keywords.el	Sun Jun 23 21:15:42 2013 +0200
     3.2 +++ b/etc/isar-keywords.el	Sun Jun 23 21:23:36 2013 +0200
     3.3 @@ -206,6 +206,7 @@
     3.4      "print_quotmapsQ3"
     3.5      "print_rules"
     3.6      "print_simpset"
     3.7 +    "print_state"
     3.8      "print_statement"
     3.9      "print_syntax"
    3.10      "print_theorems"
    3.11 @@ -374,6 +375,7 @@
    3.12      "kill"
    3.13      "kill_thy"
    3.14      "linear_undo"
    3.15 +    "pr"
    3.16      "pretty_setmargin"
    3.17      "quit"
    3.18      "remove_thy"
    3.19 @@ -398,7 +400,6 @@
    3.20      "help"
    3.21      "locale_deps"
    3.22      "nitpick"
    3.23 -    "pr"
    3.24      "prf"
    3.25      "print_abbrevs"
    3.26      "print_antiquotations"
    3.27 @@ -435,6 +436,7 @@
    3.28      "print_quotmapsQ3"
    3.29      "print_rules"
    3.30      "print_simpset"
    3.31 +    "print_state"
    3.32      "print_statement"
    3.33      "print_syntax"
    3.34      "print_theorems"
     4.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Sun Jun 23 21:15:42 2013 +0200
     4.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sun Jun 23 21:23:36 2013 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4      @{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.5      @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.6      @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     4.7 -    @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     4.8 +    @{command_def "print_state"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     4.9    \end{matharray}
    4.10  
    4.11    These diagnostic commands assist interactive development by printing
    4.12 @@ -57,7 +57,7 @@
    4.13      ;
    4.14      ( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
    4.15      ;
    4.16 -    @@{command pr} @{syntax modes}? @{syntax nat}?
    4.17 +    @@{command print_state} @{syntax modes}?
    4.18      ;
    4.19  
    4.20      @{syntax_def modes}: '(' (@{syntax name} + ) ')'
    4.21 @@ -99,11 +99,8 @@
    4.22    compact proof term, which is denoted by ``@{text _}'' placeholders
    4.23    there.
    4.24  
    4.25 -  \item @{command "pr"}~@{text "goals"} prints the current proof state
    4.26 -  (if present), including current facts and goals.  The optional limit
    4.27 -  arguments affect the number of goals to be displayed, which is
    4.28 -  initially 10.  Omitting limit value leaves the current setting
    4.29 -  unchanged.
    4.30 +  \item @{command "print_state"} prints the current proof state (if
    4.31 +  present), including current facts and goals.
    4.32  
    4.33    \end{description}
    4.34  
    4.35 @@ -111,8 +108,8 @@
    4.36    to be specified, which is appended to the current print mode; see
    4.37    also \secref{sec:print-modes}.  Thus the output behavior may be
    4.38    modified according particular print mode features.  For example,
    4.39 -  @{command "pr"}~@{text "(latex xsymbols)"} would print the current
    4.40 -  proof state with mathematical symbols and special characters
    4.41 +  @{command "print_state"}~@{text "(latex xsymbols)"} prints the
    4.42 +  current proof state with mathematical symbols and special characters
    4.43    represented in {\LaTeX} source, according to the Isabelle style
    4.44    \cite{isabelle-sys}.
    4.45  
     5.1 --- a/src/Doc/IsarRef/Quick_Reference.thy	Sun Jun 23 21:15:42 2013 +0200
     5.2 +++ b/src/Doc/IsarRef/Quick_Reference.thy	Sun Jun 23 21:23:36 2013 +0200
     5.3 @@ -98,7 +98,7 @@
     5.4  
     5.5  text {*
     5.6    \begin{tabular}{ll}
     5.7 -    @{command "pr"} & print current state \\
     5.8 +    @{command "print_state"} & print current state \\
     5.9      @{command "thm"}~@{text a} & print fact \\
    5.10      @{command "prop"}~@{text \<phi>} & print proposition \\
    5.11      @{command "term"}~@{text t} & print term \\
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jun 23 21:15:42 2013 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 23 21:23:36 2013 +0200
     6.3 @@ -969,7 +969,14 @@
     6.4      "print raw source files with symbols"
     6.5      (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
     6.6  
     6.7 -val _ =  (* FIXME tty only *)
     6.8 +val _ =
     6.9 +  Outer_Syntax.improper_command @{command_spec "print_state"}
    6.10 +    "print current proof state (if present)"
    6.11 +    (opt_modes >> (fn modes =>
    6.12 +      Toplevel.keep (fn state =>
    6.13 +        Print_Mode.with_modes modes (Toplevel.print_state true) state)));
    6.14 +
    6.15 +val _ = (*historical, e.g. for ProofGeneral-3.7.x*)
    6.16    Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
    6.17      (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
    6.18        Toplevel.keep (fn state =>
     7.1 --- a/src/Pure/Pure.thy	Sun Jun 23 21:15:42 2013 +0200
     7.2 +++ b/src/Pure/Pure.thy	Sun Jun 23 21:23:36 2013 +0200
     7.3 @@ -86,8 +86,8 @@
     7.4    and "cd" :: control
     7.5    and "pwd" :: diag
     7.6    and "use_thy" "remove_thy" "kill_thy" :: control
     7.7 -  and "display_drafts" "print_drafts" "pr" :: diag
     7.8 -  and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
     7.9 +  and "display_drafts" "print_drafts" "print_state" :: diag
    7.10 +  and "pr" "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    7.11    and "welcome" :: diag
    7.12    and "init_toplevel" "linear_undo" "undo" "undos_proof" "cannot_undo" "kill" :: control
    7.13    and "end" :: thy_end % "theory"