discontinued obsolete ProofContext.prems_limit;
authorwenzelm
Mon Sep 06 22:31:54 2010 +0200 (2010-09-06 ago)
changeset 39165e790a5560834
parent 39164 e7e12555e763
child 39166 19efc2af3e6c
discontinued obsolete ProofContext.prems_limit;
simplified command setup for 'pr' etc.;
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/preferences.ML
     1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Sep 06 22:08:49 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Sep 06 22:31:54 2010 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      ;
     1.5      ( 'prf' | 'full\_prf' ) modes? thmrefs?
     1.6      ;
     1.7 -    'pr' modes? nat? (',' nat)?
     1.8 +    'pr' modes? nat?
     1.9      ;
    1.10  
    1.11      modes: '(' (name + ) ')'
    1.12 @@ -69,11 +69,11 @@
    1.13    compact proof term, which is denoted by ``@{text _}'' placeholders
    1.14    there.
    1.15  
    1.16 -  \item @{command "pr"}~@{text "goals, prems"} prints the current
    1.17 -  proof state (if present), including the proof context, current facts
    1.18 -  and goals.  The optional limit arguments affect the number of goals
    1.19 -  and premises to be displayed, which is initially 10 for both.
    1.20 -  Omitting limit values leaves the current setting unchanged.
    1.21 +  \item @{command "pr"}~@{text "goals"} prints the current proof state
    1.22 +  (if present), including current facts and goals.  The optional limit
    1.23 +  arguments affect the number of goals to be displayed, which is
    1.24 +  initially 10.  Omitting limit value leaves the current setting
    1.25 +  unchanged.
    1.26  
    1.27    \end{description}
    1.28  
     2.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:08:49 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:31:54 2010 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4      ;
     2.5      ( 'prf' | 'full\_prf' ) modes? thmrefs?
     2.6      ;
     2.7 -    'pr' modes? nat? (',' nat)?
     2.8 +    'pr' modes? nat?
     2.9      ;
    2.10  
    2.11      modes: '(' (name + ) ')'
    2.12 @@ -90,11 +90,11 @@
    2.13    compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
    2.14    there.
    2.15  
    2.16 -  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current
    2.17 -  proof state (if present), including the proof context, current facts
    2.18 -  and goals.  The optional limit arguments affect the number of goals
    2.19 -  and premises to be displayed, which is initially 10 for both.
    2.20 -  Omitting limit values leaves the current setting unchanged.
    2.21 +  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
    2.22 +  (if present), including current facts and goals.  The optional limit
    2.23 +  arguments affect the number of goals to be displayed, which is
    2.24 +  initially 10.  Omitting limit value leaves the current setting
    2.25 +  unchanged.
    2.26  
    2.27    \end{description}
    2.28  
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Sep 06 22:08:49 2010 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Sep 06 22:31:54 2010 +0200
     3.3 @@ -34,9 +34,6 @@
     3.4    val immediate_proof: Toplevel.transition -> Toplevel.transition
     3.5    val done_proof: Toplevel.transition -> Toplevel.transition
     3.6    val skip_proof: Toplevel.transition -> Toplevel.transition
     3.7 -  val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
     3.8 -  val disable_pr: Toplevel.transition -> Toplevel.transition
     3.9 -  val enable_pr: Toplevel.transition -> Toplevel.transition
    3.10    val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    3.11    val diag_state: unit -> Toplevel.state
    3.12    val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    3.13 @@ -266,21 +263,6 @@
    3.14  val skip_proof = local_skip_proof o global_skip_proof;
    3.15  
    3.16  
    3.17 -(* print state *)
    3.18 -
    3.19 -fun set_limit _ NONE = ()
    3.20 -  | set_limit r (SOME n) = r := n;
    3.21 -
    3.22 -fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
    3.23 - (set_limit Goal_Display.goals_limit_default lim1;
    3.24 -  set_limit ProofContext.prems_limit lim2;
    3.25 -  Toplevel.quiet := false;
    3.26 -  Print_Mode.with_modes modes (Toplevel.print_state true) state));
    3.27 -
    3.28 -val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
    3.29 -val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
    3.30 -
    3.31 -
    3.32  (* diagnostic ML evaluation *)
    3.33  
    3.34  structure Diag_State = Proof_Data
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:08:49 2010 +0200
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:31:54 2010 +0200
     4.3 @@ -964,20 +964,21 @@
     4.4    Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
     4.5      Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
     4.6  
     4.7 -val opt_limits =
     4.8 -  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
     4.9 -
    4.10 -val _ =
    4.11 +val _ =  (* FIXME tty only *)
    4.12    Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
    4.13 -    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
    4.14 +    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
    4.15 +      Toplevel.no_timing o Toplevel.keep (fn state =>
    4.16 +       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
    4.17 +        Toplevel.quiet := false;
    4.18 +        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
    4.19  
    4.20  val _ =
    4.21    Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
    4.22 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
    4.23 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
    4.24  
    4.25  val _ =
    4.26    Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
    4.27 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
    4.28 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
    4.29  
    4.30  val _ =
    4.31    Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
     5.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 06 22:08:49 2010 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 06 22:31:54 2010 +0200
     5.3 @@ -144,7 +144,6 @@
     5.4    val print_cases: Proof.context -> unit
     5.5    val debug: bool Unsynchronized.ref
     5.6    val verbose: bool Unsynchronized.ref
     5.7 -  val prems_limit: int Unsynchronized.ref
     5.8    val pretty_ctxt: Proof.context -> Pretty.T list
     5.9    val pretty_context: Proof.context -> Pretty.T list
    5.10  end;
    5.11 @@ -1403,10 +1402,9 @@
    5.12  
    5.13  val debug = Unsynchronized.ref false;
    5.14  val verbose = Unsynchronized.ref false;
    5.15 -val prems_limit = Unsynchronized.ref ~1;
    5.16  
    5.17  fun pretty_ctxt ctxt =
    5.18 -  if ! prems_limit < 0 andalso not (! debug) then []
    5.19 +  if not (! debug) then []
    5.20    else
    5.21      let
    5.22        val prt_term = Syntax.pretty_term ctxt;
    5.23 @@ -1432,12 +1430,9 @@
    5.24  
    5.25        (*prems*)
    5.26        val prems = Assumption.all_prems_of ctxt;
    5.27 -      val len = length prems;
    5.28 -      val suppressed = len - ! prems_limit;
    5.29        val prt_prems =
    5.30          if null prems then []
    5.31 -        else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
    5.32 -          map (Display.pretty_thm ctxt) (drop suppressed prems))];
    5.33 +        else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)];
    5.34      in prt_structs @ prt_fixes @ prt_prems end;
    5.35  
    5.36  
     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Mon Sep 06 22:08:49 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Mon Sep 06 22:31:54 2010 +0200
     6.3 @@ -137,9 +137,6 @@
     6.4   [nat_pref Goal_Display.goals_limit_default
     6.5      "goals-limit"
     6.6      "Setting for maximum number of goals printed",
     6.7 -  int_pref ProofContext.prems_limit
     6.8 -    "prems-limit"
     6.9 -    "Setting for maximum number of premises printed",
    6.10    print_depth_pref,
    6.11    bool_pref show_question_marks_default
    6.12      "show-question-marks"