# HG changeset patch # User wenzelm # Date 1283805114 -7200 # Node ID e790a5560834301d5a1bf68d9be9974ed745c727 # Parent e7e12555e7637d50d44a200928a3fcffe48ddea7 discontinued obsolete ProofContext.prems_limit; simplified command setup for 'pr' etc.; diff -r e7e12555e763 -r e790a5560834 doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Sep 06 22:08:49 2010 +0200 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Mon Sep 06 22:31:54 2010 +0200 @@ -33,7 +33,7 @@ ; ( 'prf' | 'full\_prf' ) modes? thmrefs? ; - 'pr' modes? nat? (',' nat)? + 'pr' modes? nat? ; modes: '(' (name + ) ')' @@ -69,11 +69,11 @@ compact proof term, which is denoted by ``@{text _}'' placeholders there. - \item @{command "pr"}~@{text "goals, prems"} prints the current - proof state (if present), including the proof context, current facts - and goals. The optional limit arguments affect the number of goals - and premises to be displayed, which is initially 10 for both. - Omitting limit values leaves the current setting unchanged. + \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. \end{description} diff -r e7e12555e763 -r e790a5560834 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 22:08:49 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Mon Sep 06 22:31:54 2010 +0200 @@ -55,7 +55,7 @@ ; ( 'prf' | 'full\_prf' ) modes? thmrefs? ; - 'pr' modes? nat? (',' nat)? + 'pr' modes? nat? ; modes: '(' (name + ) ')' @@ -90,11 +90,11 @@ compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there. - \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current - proof state (if present), including the proof context, current facts - and goals. The optional limit arguments affect the number of goals - and premises to be displayed, which is initially 10 for both. - Omitting limit values leaves the current setting unchanged. + \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} 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. \end{description} diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Sep 06 22:08:49 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 06 22:31:54 2010 +0200 @@ -34,9 +34,6 @@ val immediate_proof: Toplevel.transition -> Toplevel.transition val done_proof: Toplevel.transition -> Toplevel.transition val skip_proof: Toplevel.transition -> Toplevel.transition - val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition - val disable_pr: Toplevel.transition -> Toplevel.transition - val enable_pr: Toplevel.transition -> Toplevel.transition val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition val diag_state: unit -> Toplevel.state val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm} @@ -266,21 +263,6 @@ val skip_proof = local_skip_proof o global_skip_proof; -(* print state *) - -fun set_limit _ NONE = () - | set_limit r (SOME n) = r := n; - -fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => - (set_limit Goal_Display.goals_limit_default lim1; - set_limit ProofContext.prems_limit lim2; - Toplevel.quiet := false; - Print_Mode.with_modes modes (Toplevel.print_state true) state)); - -val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true); -val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false); - - (* diagnostic ML evaluation *) structure Diag_State = Proof_Data diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Sep 06 22:08:49 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Sep 06 22:31:54 2010 +0200 @@ -964,20 +964,21 @@ Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols" Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts)); -val opt_limits = - Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat); - -val _ = +val _ = (* FIXME tty only *) Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag - (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr)); + (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) => + Toplevel.no_timing o Toplevel.keep (fn state => + (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n; + Toplevel.quiet := false; + Print_Mode.with_modes modes (Toplevel.print_state true) state)))); val _ = Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr)); + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true))); val _ = Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr)); + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false))); val _ = Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Sep 06 22:08:49 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Sep 06 22:31:54 2010 +0200 @@ -144,7 +144,6 @@ val print_cases: Proof.context -> unit val debug: bool Unsynchronized.ref val verbose: bool Unsynchronized.ref - val prems_limit: int Unsynchronized.ref val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list end; @@ -1403,10 +1402,9 @@ val debug = Unsynchronized.ref false; val verbose = Unsynchronized.ref false; -val prems_limit = Unsynchronized.ref ~1; fun pretty_ctxt ctxt = - if ! prems_limit < 0 andalso not (! debug) then [] + if not (! debug) then [] else let val prt_term = Syntax.pretty_term ctxt; @@ -1432,12 +1430,9 @@ (*prems*) val prems = Assumption.all_prems_of ctxt; - val len = length prems; - val suppressed = len - ! prems_limit; val prt_prems = if null prems then [] - else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @ - map (Display.pretty_thm ctxt) (drop suppressed prems))]; + else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)]; in prt_structs @ prt_fixes @ prt_prems end; diff -r e7e12555e763 -r e790a5560834 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Mon Sep 06 22:08:49 2010 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Mon Sep 06 22:31:54 2010 +0200 @@ -137,9 +137,6 @@ [nat_pref Goal_Display.goals_limit_default "goals-limit" "Setting for maximum number of goals printed", - int_pref ProofContext.prems_limit - "prems-limit" - "Setting for maximum number of premises printed", print_depth_pref, bool_pref show_question_marks_default "show-question-marks"