# HG changeset patch
# User wenzelm
# Date 1185980355 -7200
# Node ID 464f260e5a20d80fae8b0c750a413d204bab3827
# Parent  94210ad252e3bf5919259eac6c5fd715ad8f963e
multithreading trace: int;

diff -r 94210ad252e3 -r 464f260e5a20 lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Aug 01 16:55:45 2007 +0200
+++ b/lib/Tools/usedir	Wed Aug 01 16:59:15 2007 +0200
@@ -20,7 +20,7 @@
   echo "    -D PATH      dump generated document sources into PATH"
   echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
   echo "    -P PATH      set path for remote theory browsing information"
-  echo "    -T BOOL      multithreading: trace mode (default false)"
+  echo "    -T LEVEL     multithreading: trace level (default 0)"
   echo "    -V VERSION   declare alternative document VERSION"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -c BOOL      tell ML system to compress output image (default true)"
@@ -67,7 +67,7 @@
 DUMP=""
 MAXTHREADS="1"
 RPATH=""
-TRACETHREADS=false
+TRACETHREADS="0"
 DOCUMENT_VERSIONS=""
 BUILD=""
 COMPRESS=true
@@ -102,7 +102,7 @@
         RPATH="$OPTARG"
         ;;
       T)
-        check_bool "$OPTARG"
+        check_number "$OPTARG"
         TRACETHREADS="$OPTARG"
         ;;
       V)
diff -r 94210ad252e3 -r 464f260e5a20 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed Aug 01 16:55:45 2007 +0200
+++ b/src/Pure/Isar/session.ML	Wed Aug 01 16:59:15 2007 +0200
@@ -10,7 +10,7 @@
   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 -> bool -> unit
+    string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
   val finish: unit -> unit
 end;
 
diff -r 94210ad252e3 -r 464f260e5a20 src/Pure/ML-Systems/multithreading_dummy.ML
--- a/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Aug 01 16:55:45 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Aug 01 16:59:15 2007 +0200
@@ -14,8 +14,8 @@
 
 signature MULTITHREADING =
 sig
-  val trace: bool ref
-  val tracing: (unit -> string) -> unit
+  val trace: int ref
+  val tracing: int -> (unit -> string) -> unit
   val available: bool
   val max_threads: int ref
   val self_critical: unit -> bool
@@ -27,8 +27,8 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-val trace = ref false;
-fun tracing _ = ();
+val trace = ref 0;
+fun tracing _ _ = ();
 
 val available = false;
 val max_threads = ref 1;