src/Pure/goal_display.ML
changeset 39134 917b4b6ba3d2
parent 39125 f45d332a90e3
child 39163 4d701c0388c3
     1.1 --- a/src/Pure/goal_display.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -77,12 +77,20 @@
     1.4  
     1.5  fun pretty_goals ctxt0 state =
     1.6    let
     1.7 -    val ctxt = Config.put show_free_types false ctxt0;
     1.8 +    val ctxt = ctxt0
     1.9 +      |> Config.put show_free_types false
    1.10 +      |> Config.put show_types
    1.11 +       (Config.get ctxt0 show_types orelse
    1.12 +        Config.get ctxt0 show_sorts orelse
    1.13 +        Config.get ctxt0 show_all_types)
    1.14 +      |> Config.put show_sorts false;
    1.15  
    1.16 -    val show_all_types = Config.get ctxt show_all_types;
    1.17 +    val show_sorts0 = Config.get ctxt0 show_sorts;
    1.18 +    val show_types = Config.get ctxt show_types;
    1.19 +    val show_consts = Config.get ctxt show_consts
    1.20 +    val show_main_goal = Config.get ctxt show_main_goal;
    1.21      val goals_limit = Config.get ctxt goals_limit;
    1.22      val goals_total = Config.get ctxt goals_total;
    1.23 -    val show_main_goal = Config.get ctxt show_main_goal;
    1.24  
    1.25      val prt_sort = Syntax.pretty_sort ctxt;
    1.26      val prt_typ = Syntax.pretty_typ ctxt;
    1.27 @@ -120,23 +128,18 @@
    1.28      val {prop, tpairs, ...} = Thm.rep_thm state;
    1.29      val (As, B) = Logic.strip_horn prop;
    1.30      val ngoals = length As;
    1.31 -
    1.32 -    fun pretty_gs (types, sorts) =
    1.33 -      (if show_main_goal then [prt_term B] else []) @
    1.34 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
    1.35 -        else if ngoals > goals_limit then
    1.36 -          pretty_subgoals (take goals_limit As) @
    1.37 -          (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    1.38 -           else [])
    1.39 -        else pretty_subgoals As) @
    1.40 -      pretty_ffpairs tpairs @
    1.41 -      (if Config.get ctxt show_consts then pretty_consts prop else []) @
    1.42 -      (if types then pretty_vars prop else []) @
    1.43 -      (if sorts then pretty_varsT prop else []);
    1.44    in
    1.45 -    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
    1.46 -      (setmp_CRITICAL show_sorts false pretty_gs)
    1.47 -   (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
    1.48 +    (if show_main_goal then [prt_term B] else []) @
    1.49 +     (if ngoals = 0 then [Pretty.str "No subgoals!"]
    1.50 +      else if ngoals > goals_limit then
    1.51 +        pretty_subgoals (take goals_limit As) @
    1.52 +        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
    1.53 +         else [])
    1.54 +      else pretty_subgoals As) @
    1.55 +    pretty_ffpairs tpairs @
    1.56 +    (if show_consts then pretty_consts prop else []) @
    1.57 +    (if show_types then pretty_vars prop else []) @
    1.58 +    (if show_sorts0 then pretty_varsT prop else [])
    1.59    end;
    1.60  
    1.61  fun pretty_goals_without_context th =