src/Pure/Isar/session.ML
changeset 24612 d1b315bdb8d7
parent 24118 464f260e5a20
child 25703 832073e402ae
equal deleted inserted replaced
24611:1f92518fbabe 24612:d1b315bdb8d7
    85       Present.init build info doc doc_graph doc_versions (path ()) name
    85       Present.init build info doc doc_graph doc_versions (path ()) name
    86         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
    86         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
    87       Secure.use_noncritical root;
    87       Secure.use_noncritical root;
    88       finish ()))
    88       finish ()))
    89     |> setmp_noncritical Proofterm.proofs level
    89     |> setmp_noncritical Proofterm.proofs level
    90     |> setmp_noncritical print_mode (modes @ ! print_mode)
    90     |> setmp_noncritical print_mode (modes @ print_mode_value ())
    91     |> setmp_noncritical Multithreading.trace trace_threads
    91     |> setmp_noncritical Multithreading.trace trace_threads
    92     |> setmp_noncritical Multithreading.max_threads
    92     |> setmp_noncritical Multithreading.max_threads
    93       (if Multithreading.available then max_threads
    93       (if Multithreading.available then max_threads
    94        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
    94        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
    95   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
    95   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);