1.1 --- a/lib/Tools/usedir	Wed Aug 01 16:55:45 2007 +0200
     1.2 +++ b/lib/Tools/usedir	Wed Aug 01 16:59:15 2007 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    echo "    -D PATH      dump generated document sources into PATH"
     1.5    echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
     1.6    echo "    -P PATH      set path for remote theory browsing information"
     1.7 -  echo "    -T BOOL      multithreading: trace mode (default false)"
     1.8 +  echo "    -T LEVEL     multithreading: trace level (default 0)"
     1.9    echo "    -V VERSION   declare alternative document VERSION"
    1.10    echo "    -b           build mode (output heap image, using current dir)"
    1.11    echo "    -c BOOL      tell ML system to compress output image (default true)"
    1.12 @@ -67,7 +67,7 @@
    1.13  DUMP=""
    1.14  MAXTHREADS="1"
    1.15  RPATH=""
    1.16 -TRACETHREADS=false
    1.17 +TRACETHREADS="0"
    1.18  DOCUMENT_VERSIONS=""
    1.19  BUILD=""
    1.20  COMPRESS=true
    1.21 @@ -102,7 +102,7 @@
    1.22          RPATH="$OPTARG"
    1.23          ;;
    1.24        T)
    1.25 -        check_bool "$OPTARG"
    1.26 +        check_number "$OPTARG"
    1.27          TRACETHREADS="$OPTARG"
    1.28          ;;
    1.29        V)

     2.1 --- a/src/Pure/Isar/session.ML	Wed Aug 01 16:55:45 2007 +0200
     2.2 +++ b/src/Pure/Isar/session.ML	Wed Aug 01 16:59:15 2007 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val name: unit -> string
     2.5    val welcome: unit -> string
     2.6    val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
     2.7 -    string -> string -> bool * string -> string -> int -> bool -> int -> bool -> unit
     2.8 +    string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
     2.9    val finish: unit -> unit
    2.10  end;
    2.11  

     3.1 --- a/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Aug 01 16:55:45 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Aug 01 16:59:15 2007 +0200
     3.3 @@ -14,8 +14,8 @@
     3.4  
     3.5  signature MULTITHREADING =
     3.6  sig
     3.7 -  val trace: bool ref
     3.8 -  val tracing: (unit -> string) -> unit
     3.9 +  val trace: int ref
    3.10 +  val tracing: int -> (unit -> string) -> unit
    3.11    val available: bool
    3.12    val max_threads: int ref
    3.13    val self_critical: unit -> bool
    3.14 @@ -27,8 +27,8 @@
    3.15  structure Multithreading: MULTITHREADING =
    3.16  struct
    3.17  
    3.18 -val trace = ref false;
    3.19 -fun tracing _ = ();
    3.20 +val trace = ref 0;
    3.21 +fun tracing _ _ = ();
    3.22  
    3.23  val available = false;
    3.24  val max_threads = ref 1;