--- a/NEWS Sun Jun 23 21:15:42 2013 +0200
+++ b/NEWS Sun Jun 23 21:23:36 2013 +0200
@@ -32,6 +32,10 @@
* Updated and extended "isar-ref" and "implementation" manual,
eliminated old "ref" manual.
+* Proper diagnostic command 'print_state'. Old 'pr' (with its
+implicit change of some global references) is retained for now as
+control command, e.g. for ProofGeneral 3.7.x.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/etc/isar-keywords-ZF.el Sun Jun 23 21:15:42 2013 +0200
+++ b/etc/isar-keywords-ZF.el Sun Jun 23 21:23:36 2013 +0200
@@ -143,6 +143,7 @@
"print_options"
"print_rules"
"print_simpset"
+ "print_state"
"print_statement"
"print_syntax"
"print_tcset"
@@ -267,6 +268,7 @@
"kill"
"kill_thy"
"linear_undo"
+ "pr"
"pretty_setmargin"
"quit"
"remove_thy"
@@ -286,7 +288,6 @@
"header"
"help"
"locale_deps"
- "pr"
"prf"
"print_abbrevs"
"print_antiquotations"
@@ -311,6 +312,7 @@
"print_options"
"print_rules"
"print_simpset"
+ "print_state"
"print_statement"
"print_syntax"
"print_tcset"
--- a/etc/isar-keywords.el Sun Jun 23 21:15:42 2013 +0200
+++ b/etc/isar-keywords.el Sun Jun 23 21:23:36 2013 +0200
@@ -206,6 +206,7 @@
"print_quotmapsQ3"
"print_rules"
"print_simpset"
+ "print_state"
"print_statement"
"print_syntax"
"print_theorems"
@@ -374,6 +375,7 @@
"kill"
"kill_thy"
"linear_undo"
+ "pr"
"pretty_setmargin"
"quit"
"remove_thy"
@@ -398,7 +400,6 @@
"help"
"locale_deps"
"nitpick"
- "pr"
"prf"
"print_abbrevs"
"print_antiquotations"
@@ -435,6 +436,7 @@
"print_quotmapsQ3"
"print_rules"
"print_simpset"
+ "print_state"
"print_statement"
"print_syntax"
"print_theorems"
--- a/src/Doc/IsarRef/Inner_Syntax.thy Sun Jun 23 21:15:42 2013 +0200
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Sun Jun 23 21:23:36 2013 +0200
@@ -40,7 +40,7 @@
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+ @{command_def "print_state"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
\end{matharray}
These diagnostic commands assist interactive development by printing
@@ -57,7 +57,7 @@
;
( @@{command prf} | @@{command full_prf} ) @{syntax modes}? @{syntax thmrefs}?
;
- @@{command pr} @{syntax modes}? @{syntax nat}?
+ @@{command print_state} @{syntax modes}?
;
@{syntax_def modes}: '(' (@{syntax name} + ) ')'
@@ -99,11 +99,8 @@
compact proof term, which is denoted by ``@{text _}'' placeholders
there.
- \item @{command "pr"}~@{text "goals"} prints the current proof state
- (if present), including current facts and goals. The optional limit
- arguments affect the number of goals to be displayed, which is
- initially 10. Omitting limit value leaves the current setting
- unchanged.
+ \item @{command "print_state"} prints the current proof state (if
+ present), including current facts and goals.
\end{description}
@@ -111,8 +108,8 @@
to be specified, which is appended to the current print mode; see
also \secref{sec:print-modes}. Thus the output behavior may be
modified according particular print mode features. For example,
- @{command "pr"}~@{text "(latex xsymbols)"} would print the current
- proof state with mathematical symbols and special characters
+ @{command "print_state"}~@{text "(latex xsymbols)"} prints the
+ current proof state with mathematical symbols and special characters
represented in {\LaTeX} source, according to the Isabelle style
\cite{isabelle-sys}.
--- a/src/Doc/IsarRef/Quick_Reference.thy Sun Jun 23 21:15:42 2013 +0200
+++ b/src/Doc/IsarRef/Quick_Reference.thy Sun Jun 23 21:23:36 2013 +0200
@@ -98,7 +98,7 @@
text {*
\begin{tabular}{ll}
- @{command "pr"} & print current state \\
+ @{command "print_state"} & print current state \\
@{command "thm"}~@{text a} & print fact \\
@{command "prop"}~@{text \<phi>} & print proposition \\
@{command "term"}~@{text t} & print term \\
--- a/src/Pure/Isar/isar_syn.ML Sun Jun 23 21:15:42 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Jun 23 21:23:36 2013 +0200
@@ -969,7 +969,14 @@
"print raw source files with symbols"
(Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
-val _ = (* FIXME tty only *)
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_state"}
+ "print current proof state (if present)"
+ (opt_modes >> (fn modes =>
+ Toplevel.keep (fn state =>
+ Print_Mode.with_modes modes (Toplevel.print_state true) state)));
+
+val _ = (*historical, e.g. for ProofGeneral-3.7.x*)
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 =>
--- a/src/Pure/Pure.thy Sun Jun 23 21:15:42 2013 +0200
+++ b/src/Pure/Pure.thy Sun Jun 23 21:23:36 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" "pr" :: diag
- and "pretty_setmargin" "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+ and "display_drafts" "print_drafts" "print_state" :: diag
+ and "pr" "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"