etc/options
changeset 67138 82283d52b4d6
parent 67137 f2384ad1dff4
child 67191 9ab34bb83a84
equal deleted inserted replaced
67137:f2384ad1dff4 67138:82283d52b4d6
     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   -- "alternative document variants (separated by colons)"
    13   -- "alternative document variants (separated by colons)"
       
    14 option document_tags : string = ""
       
    15   -- "default command tags (separated by commas)"
    14 
    16 
    15 option thy_output_display : bool = false
    17 option thy_output_display : bool = false
    16   -- "indicate output as multi-line display-style material"
    18   -- "indicate output as multi-line display-style material"
    17 option thy_output_break : bool = false
    19 option thy_output_break : bool = false
    18   -- "control line breaks in non-display material"
    20   -- "control line breaks in non-display material"