6 *) |
6 *) |
7 |
7 |
8 signature GOAL_DISPLAY = |
8 signature GOAL_DISPLAY = |
9 sig |
9 sig |
10 val goals_limit_default: int Unsynchronized.ref |
10 val goals_limit_default: int Unsynchronized.ref |
11 val goals_limit_value: Config.value Config.T |
11 val goals_limit_raw: Config.raw |
12 val goals_limit: int Config.T |
12 val goals_limit: int Config.T |
13 val goals_total: bool Config.T |
13 val goals_total: bool Config.T |
14 val show_main_goal_default: bool Unsynchronized.ref |
14 val show_main_goal_default: bool Unsynchronized.ref |
15 val show_main_goal_value: Config.value Config.T |
15 val show_main_goal_raw: Config.raw |
16 val show_main_goal: bool Config.T |
16 val show_main_goal: bool Config.T |
17 val show_consts_default: bool Unsynchronized.ref |
17 val show_consts_default: bool Unsynchronized.ref |
18 val show_consts_value: Config.value Config.T |
18 val show_consts_raw: Config.raw |
19 val show_consts: bool Config.T |
19 val show_consts: bool Config.T |
20 val pretty_flexpair: Proof.context -> term * term -> Pretty.T |
20 val pretty_flexpair: Proof.context -> term * term -> Pretty.T |
21 val pretty_goals: Proof.context -> thm -> Pretty.T list |
21 val pretty_goals: Proof.context -> thm -> Pretty.T list |
22 val pretty_goals_without_context: thm -> Pretty.T list |
22 val pretty_goals_without_context: thm -> Pretty.T list |
23 end; |
23 end; |
24 |
24 |
25 structure Goal_Display: GOAL_DISPLAY = |
25 structure Goal_Display: GOAL_DISPLAY = |
26 struct |
26 struct |
27 |
27 |
28 val goals_limit_default = Unsynchronized.ref 10; |
28 val goals_limit_default = Unsynchronized.ref 10; |
29 val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default)); |
29 val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default)); |
30 val goals_limit = Config.int goals_limit_value; |
30 val goals_limit = Config.int goals_limit_raw; |
31 |
31 |
32 val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true)); |
32 val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true)); |
33 |
33 |
34 val show_main_goal_default = Unsynchronized.ref false; |
34 val show_main_goal_default = Unsynchronized.ref false; |
35 val show_main_goal_value = |
35 val show_main_goal_raw = |
36 Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default)); |
36 Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default)); |
37 val show_main_goal = Config.bool show_main_goal_value; |
37 val show_main_goal = Config.bool show_main_goal_raw; |
38 |
38 |
39 val show_consts_default = Unsynchronized.ref false; |
39 val show_consts_default = Unsynchronized.ref false; |
40 val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default)); |
40 val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default)); |
41 val show_consts = Config.bool show_consts_value; |
41 val show_consts = Config.bool show_consts_raw; |
42 |
42 |
43 fun pretty_flexpair ctxt (t, u) = Pretty.block |
43 fun pretty_flexpair ctxt (t, u) = Pretty.block |
44 [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; |
44 [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; |
45 |
45 |
46 |
46 |