# HG changeset patch
# User wenzelm
# Date 1248429035 -7200
# Node ID d32817dda0e64fb9e6706109b7776dbd85a1103c
# Parent  95ffc6e2a0ea153f3db4f3040353eba81272ce1e
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;

diff -r 95ffc6e2a0ea -r d32817dda0e6 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Jul 24 11:31:22 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Jul 24 11:50:35 2009 +0200
@@ -140,7 +140,7 @@
 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
 
 fun pr_goals ctxt st =
-    Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
+    Display_Goal.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
      |> Pretty.chunks
      |> Pretty.string_of
 
diff -r 95ffc6e2a0ea -r d32817dda0e6 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Jul 24 11:31:22 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Jul 24 11:50:35 2009 +0200
@@ -344,8 +344,8 @@
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
             description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          Display_Goal.pretty_goals ctxt Markup.subgoal
-            (true, ! show_main_goal) (! Display.goals_limit) goal @
+          Display_Goal.pretty_goals ctxt
+            {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
 
@@ -365,8 +365,10 @@
   end;
 
 fun pretty_goals main state =
-  let val (ctxt, (_, goal)) = get_goal state
-  in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
+  let val (ctxt, (_, goal)) = get_goal state in
+    Display_Goal.pretty_goals ctxt
+      {total = false, main = main, maxgoals = ! Display.goals_limit} goal
+  end;
 
 
 
@@ -472,8 +474,8 @@
 
     val ngoals = Thm.nprems_of goal;
     val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
-      (Display_Goal.pretty_goals ctxt Markup.none
-          (true, ! show_main_goal) (! Display.goals_limit) goal @
+      (Display_Goal.pretty_goals ctxt
+          {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
         [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
diff -r 95ffc6e2a0ea -r d32817dda0e6 src/Pure/display_goal.ML
--- a/src/Pure/display_goal.ML	Fri Jul 24 11:31:22 2009 +0200
+++ b/src/Pure/display_goal.ML	Fri Jul 24 11:50:35 2009 +0200
@@ -10,7 +10,8 @@
   val goals_limit: int ref
   val show_consts: bool ref
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
-  val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
+  val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
+    thm -> Pretty.T list
   val pretty_goals_without_context: int -> thm -> Pretty.T list
   val print_goals_without_context: int -> thm -> unit
 end;
@@ -56,7 +57,7 @@
 
 in
 
-fun pretty_goals ctxt markup (msg, main) maxgoals state =
+fun pretty_goals ctxt {total, main, maxgoals} state =
   let
     val prt_sort = Syntax.pretty_sort ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
@@ -80,7 +81,7 @@
     fun pretty_list _ _ [] = []
       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
 
-    fun pretty_subgoal (n, A) = Pretty.markup markup
+    fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
       [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
 
@@ -100,7 +101,7 @@
        (if ngoals = 0 then [Pretty.str "No subgoals!"]
         else if ngoals > maxgoals then
           pretty_subgoals (Library.take (maxgoals, As)) @
-          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
            else [])
         else pretty_subgoals As) @
       pretty_ffpairs tpairs @
@@ -115,7 +116,8 @@
   end;
 
 fun pretty_goals_without_context n th =
-  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
+  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
+    {total = true, main = true, maxgoals = n} th;
 
 val print_goals_without_context =
   (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;