--- 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)
--- 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;
--- 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;