added option -T (multithreading trace mode);
authorwenzelm
Sun Jul 29 19:46:02 2007 +0200 (2007-07-29)
changeset 2406168d2b6cf5194
parent 24060 b643ee118928
child 24062 845c0d693328
added option -T (multithreading trace mode);
lib/Tools/usedir
src/Pure/Isar/session.ML
     1.1 --- a/lib/Tools/usedir	Sun Jul 29 17:28:57 2007 +0200
     1.2 +++ b/lib/Tools/usedir	Sun Jul 29 19:46:02 2007 +0200
     1.3 @@ -20,6 +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 "    -V VERSION   declare alternative document VERSION"
     1.9    echo "    -b           build mode (output heap image, using current dir)"
    1.10    echo "    -c BOOL      tell ML system to compress output image (default true)"
    1.11 @@ -62,10 +63,11 @@
    1.12  
    1.13  # options
    1.14  
    1.15 -COPY_DUMP="true"
    1.16 +COPY_DUMP=true
    1.17  DUMP=""
    1.18  MAXTHREADS="1"
    1.19  RPATH=""
    1.20 +TRACETHREADS=false
    1.21  DOCUMENT_VERSIONS=""
    1.22  BUILD=""
    1.23  COMPRESS=true
    1.24 @@ -82,7 +84,7 @@
    1.25  function getoptions()
    1.26  {
    1.27    OPTIND=1
    1.28 -  while getopts "C:D:M:P:V:bc:d:f:g:i:m:p:rs:v:" OPT
    1.29 +  while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
    1.30    do
    1.31      case "$OPT" in
    1.32        C)
    1.33 @@ -99,6 +101,10 @@
    1.34        P)
    1.35          RPATH="$OPTARG"
    1.36          ;;
    1.37 +      T)
    1.38 +        check_bool "$OPTARG"
    1.39 +        TRACETHREADS="$OPTARG"
    1.40 +        ;;
    1.41        V)
    1.42          if [ -z "$DOCUMENT_VERSIONS" ]; then
    1.43            DOCUMENT_VERSIONS="\"$OPTARG\""
    1.44 @@ -215,7 +221,7 @@
    1.45    [ "$COMPRESS" = true ] && OPT_C="-c"
    1.46  
    1.47    "$ISABELLE" \
    1.48 -    -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.49 +    -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;" \
    1.50      $OPT_C -q -w $LOGIC $NAME > "$LOG"
    1.51    RC="$?"
    1.52  else
    1.53 @@ -224,7 +230,7 @@
    1.54    LOG="$LOGDIR/$ITEM"
    1.55  
    1.56    "$ISABELLE" \
    1.57 -    -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.58 +    -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();" \
    1.59      -r -q "$LOGIC" > "$LOG"
    1.60    RC="$?"
    1.61    cd ..
     2.1 --- a/src/Pure/Isar/session.ML	Sun Jul 29 17:28:57 2007 +0200
     2.2 +++ b/src/Pure/Isar/session.ML	Sun Jul 29 19:46:02 2007 +0200
     2.3 @@ -9,8 +9,8 @@
     2.4  sig
     2.5    val name: unit -> string
     2.6    val welcome: unit -> string
     2.7 -  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
     2.8 -    string list -> string -> string -> bool * string -> string -> int -> bool -> int -> unit
     2.9 +  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
    2.10 +    string -> string -> bool * string -> string -> int -> bool -> int -> bool -> unit
    2.11    val finish: unit -> unit
    2.12  end;
    2.13  
    2.14 @@ -79,7 +79,7 @@
    2.15    | dumping (cp, path) = SOME (cp, Path.explode path);
    2.16  
    2.17  fun use_dir root build modes reset info doc doc_graph doc_versions
    2.18 -    parent name dump rpath level verbose max_threads =
    2.19 +    parent name dump rpath level verbose max_threads trace_threads =
    2.20    ((fn () =>
    2.21       (init reset parent name;
    2.22        Present.init build info doc doc_graph doc_versions (path ()) name
    2.23 @@ -88,6 +88,7 @@
    2.24        finish ()))
    2.25      |> setmp_noncritical Proofterm.proofs level
    2.26      |> setmp_noncritical print_mode (modes @ ! print_mode)
    2.27 +    |> setmp_noncritical Multithreading.trace trace_threads
    2.28      |> setmp_noncritical Multithreading.max_threads
    2.29        (if Multithreading.available then max_threads
    2.30         else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()