26 * Various options that affect pretty printing etc. are now properly |
26 * Various options that affect pretty printing etc. are now properly |
27 handled within the context via configuration options, instead of |
27 handled within the context via configuration options, instead of |
28 unsynchronized references. There are both ML Config.T entities and |
28 unsynchronized references. There are both ML Config.T entities and |
29 Isar declaration attributes to access these. |
29 Isar declaration attributes to access these. |
30 |
30 |
31 ML: Isar: |
31 ML (Config.T) Isar (attribute) |
32 |
32 |
33 Thy_Output.display thy_output_display |
33 Thy_Output.display thy_output_display |
34 Thy_Output.quotes thy_output_quotes |
34 Thy_Output.quotes thy_output_quotes |
35 Thy_Output.indent thy_output_indent |
35 Thy_Output.indent thy_output_indent |
36 Thy_Output.source thy_output_source |
36 Thy_Output.source thy_output_source |
37 Thy_Output.break thy_output_break |
37 Thy_Output.break thy_output_break |
38 |
38 |
39 show_question_marks show_question_marks |
39 show_question_marks show_question_marks |
40 show_consts show_consts |
40 show_consts show_consts |
41 |
41 |
42 Note that the corresponding "..._default" references in ML may be only |
42 Goal_Display.goals_limit goals_limit |
|
43 Goal_Display.show_main_goal show_main_goal |
|
44 |
|
45 Note that corresponding "..._default" references in ML may be only |
43 changed globally at the ROOT session setup, but *not* within a theory. |
46 changed globally at the ROOT session setup, but *not* within a theory. |
44 |
47 |
45 |
48 |
46 *** Pure *** |
49 *** Pure *** |
47 |
50 |