# HG changeset patch
# User wenzelm
# Date 1185310426 -7200
# Node ID 9c418fa38f7e90c1b4514f8cfd28a181dfc31365
# Parent  e6d505d5b03d97d82ded5076b0eb07faad17ea57
added usedir option -M: max threads;

diff -r e6d505d5b03d -r 9c418fa38f7e lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Jul 24 21:51:18 2007 +0200
+++ b/lib/Tools/usedir	Tue Jul 24 22:53:46 2007 +0200
@@ -18,6 +18,7 @@
   echo "  Options are:"
   echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
   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 "    -V VERSION   declare alternative document VERSION"
   echo "    -b           build mode (output heap image, using current dir)"
@@ -63,6 +64,7 @@
 
 COPY_DUMP="true"
 DUMP=""
+MAXTHREADS="1"
 RPATH=""
 DOCUMENT_VERSIONS=""
 BUILD=""
@@ -80,7 +82,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
+  while getopts "C:D:M:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       C)
@@ -90,6 +92,10 @@
       D)
         DUMP="$OPTARG"
         ;;
+      M)
+        check_number "$OPTARG"
+        MAXTHREADS="$OPTARG"
+        ;;
       P)
         RPATH="$OPTARG"
         ;;
@@ -209,7 +215,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;" \
+    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -218,7 +224,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; 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; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r e6d505d5b03d -r 9c418fa38f7e src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Tue Jul 24 21:51:18 2007 +0200
+++ b/src/Pure/Isar/session.ML	Tue Jul 24 22:53:46 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 -> unit
+    string list -> string -> string -> bool * string -> string -> int -> bool -> int -> unit
   val finish: unit -> unit
 end;
 
@@ -79,15 +79,16 @@
   | 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 =
-  setmp_noncritical print_mode (modes @ ! print_mode)
-    (setmp_noncritical Proofterm.proofs level (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 ()));
-       ThyInfo.time_use root;
-       finish ()))) ()
+    parent name dump rpath level verbose max_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 ()));
+      ThyInfo.time_use root;
+      finish ()))
+    |> setmp_noncritical Proofterm.proofs level
+    |> setmp_noncritical print_mode (modes @ ! print_mode)
+    |> setmp_noncritical Multithreading.max_threads max_threads) ()
   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
 
-
 end;