1.1 --- a/lib/Tools/usedir	Tue Jul 24 21:51:18 2007 +0200
     1.2 +++ b/lib/Tools/usedir	Tue Jul 24 22:53:46 2007 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    echo "  Options are:"
     1.5    echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
     1.6    echo "    -D PATH      dump generated document sources into PATH"
     1.7 +  echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
     1.8    echo "    -P PATH      set path for remote theory browsing information"
     1.9    echo "    -V VERSION   declare alternative document VERSION"
    1.10    echo "    -b           build mode (output heap image, using current dir)"
    1.11 @@ -63,6 +64,7 @@
    1.12  
    1.13  COPY_DUMP="true"
    1.14  DUMP=""
    1.15 +MAXTHREADS="1"
    1.16  RPATH=""
    1.17  DOCUMENT_VERSIONS=""
    1.18  BUILD=""
    1.19 @@ -80,7 +82,7 @@
    1.20  function getoptions()
    1.21  {
    1.22    OPTIND=1
    1.23 -  while getopts "C:D:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
    1.24 +  while getopts "C:D:M:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
    1.25    do
    1.26      case "$OPT" in
    1.27        C)
    1.28 @@ -90,6 +92,10 @@
    1.29        D)
    1.30          DUMP="$OPTARG"
    1.31          ;;
    1.32 +      M)
    1.33 +        check_number "$OPTARG"
    1.34 +        MAXTHREADS="$OPTARG"
    1.35 +        ;;
    1.36        P)
    1.37          RPATH="$OPTARG"
    1.38          ;;
    1.39 @@ -209,7 +215,7 @@
    1.40    [ "$COMPRESS" = true ] && OPT_C="-c"
    1.41  
    1.42    "$ISABELLE" \
    1.43 -    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE;" \
    1.44 +    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS;" \
    1.45      $OPT_C -q -w $LOGIC $NAME > "$LOG"
    1.46    RC="$?"
    1.47  else
    1.48 @@ -218,7 +224,7 @@
    1.49    LOG="$LOGDIR/$ITEM"
    1.50  
    1.51    "$ISABELLE" \
    1.52 -    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE; quit();" \
    1.53 +    -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();" \
    1.54      -r -q "$LOGIC" > "$LOG"
    1.55    RC="$?"
    1.56    cd ..

     2.1 --- a/src/Pure/Isar/session.ML	Tue Jul 24 21:51:18 2007 +0200
     2.2 +++ b/src/Pure/Isar/session.ML	Tue Jul 24 22:53:46 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 ->
     2.7 -    string list -> string -> string -> bool * string -> string -> int -> bool -> unit
     2.8 +    string list -> string -> string -> bool * string -> string -> int -> bool -> int -> unit
     2.9    val finish: unit -> unit
    2.10  end;
    2.11  
    2.12 @@ -79,15 +79,16 @@
    2.13    | dumping (cp, path) = SOME (cp, Path.explode path);
    2.14  
    2.15  fun use_dir root build modes reset info doc doc_graph doc_versions
    2.16 -    parent name dump rpath level verbose =
    2.17 -  setmp_noncritical print_mode (modes @ ! print_mode)
    2.18 -    (setmp_noncritical Proofterm.proofs level (fn () =>
    2.19 -      (init reset parent name;
    2.20 -       Present.init build info doc doc_graph doc_versions (path ()) name
    2.21 -         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
    2.22 -       ThyInfo.time_use root;
    2.23 -       finish ()))) ()
    2.24 +    parent name dump rpath level verbose max_threads =
    2.25 +  ((fn () =>
    2.26 +     (init reset parent name;
    2.27 +      Present.init build info doc doc_graph doc_versions (path ()) name
    2.28 +        (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
    2.29 +      ThyInfo.time_use root;
    2.30 +      finish ()))
    2.31 +    |> setmp_noncritical Proofterm.proofs level
    2.32 +    |> setmp_noncritical print_mode (modes @ ! print_mode)
    2.33 +    |> setmp_noncritical Multithreading.max_threads max_threads) ()
    2.34    handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
    2.35  
    2.36 -
    2.37  end;