# HG changeset patch
# User wenzelm
# Date 1185731162 -7200
# Node ID 68d2b6cf51948f5445abd72e4095f5c0450e7a11
# Parent  b643ee118928266d1c385e053408533a6ed13c5b
added option -T (multithreading trace mode);

diff -r b643ee118928 -r 68d2b6cf5194 lib/Tools/usedir
--- a/lib/Tools/usedir	Sun Jul 29 17:28:57 2007 +0200
+++ b/lib/Tools/usedir	Sun Jul 29 19:46:02 2007 +0200
@@ -20,6 +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 "    -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)"
@@ -62,10 +63,11 @@
 
 # options
 
-COPY_DUMP="true"
+COPY_DUMP=true
 DUMP=""
 MAXTHREADS="1"
 RPATH=""
+TRACETHREADS=false
 DOCUMENT_VERSIONS=""
 BUILD=""
 COMPRESS=true
@@ -82,7 +84,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:M:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
+  while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       C)
@@ -99,6 +101,10 @@
       P)
         RPATH="$OPTARG"
         ;;
+      T)
+        check_bool "$OPTARG"
+        TRACETHREADS="$OPTARG"
+        ;;
       V)
         if [ -z "$DOCUMENT_VERSIONS" ]; then
           DOCUMENT_VERSIONS="\"$OPTARG\""
@@ -215,7 +221,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS;" \
+    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -224,7 +230,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS; quit();" \
+    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r b643ee118928 -r 68d2b6cf5194 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Sun Jul 29 17:28:57 2007 +0200
+++ b/src/Pure/Isar/session.ML	Sun Jul 29 19:46:02 2007 +0200
@@ -9,8 +9,8 @@
 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;
 
@@ -79,7 +79,7 @@
   | 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
@@ -88,6 +88,7 @@
       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))) ()