src/Pure/Isar/session.ML

 
 signature SESSION =
 sig
   val name: unit -> string
   val welcome: unit -> string
-  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
-    string list -> string -> string -> bool * string -> string -> int -> bool -> int -> unit
+  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
+    string -> string -> bool * string -> string -> int -> bool -> int -> bool -> unit
   val finish: unit -> unit
 end;
 
 structure Session: SESSION =
 struct

 
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
 fun use_dir root build modes reset info doc doc_graph doc_versions
-    parent name dump rpath level verbose max_threads =
+    parent name dump rpath level verbose max_threads trace_threads =
   ((fn () =>
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
       Secure.use_noncritical root;
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
     |> setmp_noncritical print_mode (modes @ ! print_mode)
+    |> setmp_noncritical Multithreading.trace trace_threads
     |> setmp_noncritical Multithreading.max_threads
       (if Multithreading.available then max_threads
        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);