# HG changeset patch # User wenzelm # Date 1372015416 -7200 # Node ID 289e36c2870a9dcbd9509a001ceea94914d009c1 # Parent 921f22c8890ebcf1872b19af675c905ae3ef921e proper diagnostic command 'print_state'; diff -r 921f22c8890e -r 289e36c2870a NEWS --- 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 *** diff -r 921f22c8890e -r 289e36c2870a etc/isar-keywords-ZF.el --- 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" diff -r 921f22c8890e -r 289e36c2870a etc/isar-keywords.el --- 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" diff -r 921f22c8890e -r 289e36c2870a src/Doc/IsarRef/Inner_Syntax.thy --- 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 \"} \\ @{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \"} \\ - @{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \"} \\ + @{command_def "print_state"}@{text "\<^sup>*"} & : & @{text "any \"} \\ \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}. diff -r 921f22c8890e -r 289e36c2870a src/Doc/IsarRef/Quick_Reference.thy --- 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 \} & print proposition \\ @{command "term"}~@{text t} & print term \\ diff -r 921f22c8890e -r 289e36c2870a src/Pure/Isar/isar_syn.ML --- 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 => diff -r 921f22c8890e -r 289e36c2870a src/Pure/Pure.thy --- 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"