equal
deleted
inserted
replaced
38 |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display") |
38 |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display") |
39 |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes") |
39 |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes") |
40 |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent") |
40 |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent") |
41 |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source") |
41 |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source") |
42 |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break") |
42 |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break") |
|
43 |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin") |
43 |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing"); |
44 |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing"); |
44 |
45 |
45 fun use_theories (options, thys) = |
46 fun use_theories (options, thys) = |
46 let val condition = space_explode "," (Options.string options "condition") in |
47 let val condition = space_explode "," (Options.string options "condition") in |
47 (case filter_out (can getenv_strict) condition of |
48 (case filter_out (can getenv_strict) condition of |