equal
deleted
inserted
replaced
16 |
16 |
17 option thy_output_display : bool = false |
17 option thy_output_display : bool = false |
18 -- "indicate output as multi-line display-style material" |
18 -- "indicate output as multi-line display-style material" |
19 option thy_output_break : bool = false |
19 option thy_output_break : bool = false |
20 -- "control line breaks in non-display material" |
20 -- "control line breaks in non-display material" |
|
21 option thy_output_cartouche : bool = false |
|
22 -- "indicate if the output should be delimited as cartouche" |
21 option thy_output_quotes : bool = false |
23 option thy_output_quotes : bool = false |
22 -- "indicate if the output should be enclosed in double quotes" |
24 -- "indicate if the output should be delimited via double quotes" |
23 option thy_output_margin : int = 76 |
25 option thy_output_margin : int = 76 |
24 -- "right margin / page width for printing of display material" |
26 -- "right margin / page width for printing of display material" |
25 option thy_output_indent : int = 0 |
27 option thy_output_indent : int = 0 |
26 -- "indentation for pretty printing of display material" |
28 -- "indentation for pretty printing of display material" |
27 option thy_output_source : bool = false |
29 option thy_output_source : bool = false |