equal
deleted
inserted
replaced
8 option document : string = "" |
8 option document : string = "" |
9 -- "build document in given format: pdf, dvi, false" |
9 -- "build document in given format: pdf, dvi, false" |
10 option document_output : string = "" |
10 option document_output : string = "" |
11 -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" |
11 -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" |
12 option document_variants : string = "document" |
12 option document_variants : string = "document" |
13 -- "option alternative document variants (separated by colons)" |
13 -- "alternative document variants (separated by colons)" |
14 |
14 |
15 option thy_output_display : bool = false |
15 option thy_output_display : bool = false |
16 -- "indicate output as multi-line display-style material" |
16 -- "indicate output as multi-line display-style material" |
17 option thy_output_break : bool = false |
17 option thy_output_break : bool = false |
18 -- "control line breaks in non-display material" |
18 -- "control line breaks in non-display material" |