# HG changeset patch # User wenzelm # Date 1283553081 -7200 # Node ID 976af4e27cde26a750606f0ed55adfdf27cddba6 # Parent 93a7365fb4ee504cbe37afed67e95516f51b5251 recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e); diff -r 93a7365fb4ee -r 976af4e27cde src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Sep 03 23:54:48 2010 +0200 +++ b/src/Pure/Isar/proof.ML Sat Sep 04 00:31:21 2010 +0200 @@ -370,11 +370,11 @@ fun pretty_goals main state = let - val (ctxt, (_, goal)) = get_goal state; - val ctxt' = ctxt + val (_, (_, goal)) = get_goal state; + val ctxt = context_of state |> Config.put Goal_Display.show_main_goal main |> Config.put Goal_Display.goals_total false; - in Goal_Display.pretty_goals ctxt' goal end; + in Goal_Display.pretty_goals ctxt goal end; diff -r 93a7365fb4ee -r 976af4e27cde src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Sep 03 23:54:48 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Sep 04 00:31:21 2010 +0200 @@ -583,7 +583,8 @@ fun goal_state name main_goal = antiquotation name (Scan.succeed ()) (fn {state, context = ctxt, ...} => fn () => output ctxt - [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]); + [Pretty.chunks + (Proof.pretty_goals main_goal (Proof.map_context (K ctxt) (proof_state state)))]); in