# HG changeset patch
# User webertj
# Date 1098985222 -7200
# Node ID f856f4f3258fc3132176b9291694fd8ed32da1ce
# Parent  9e12b5443e7f547561dccc0f60f404a278199494
isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)

diff -r 9e12b5443e7f -r f856f4f3258f lib/Tools/usedir
--- a/lib/Tools/usedir	Thu Oct 28 17:11:51 2004 +0200
+++ b/lib/Tools/usedir	Thu Oct 28 19:40:22 2004 +0200
@@ -21,6 +21,7 @@
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -c BOOL      tell ML system to compress output image (default true)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
+  echo "    -f NAME      use ML file NAME (default ROOT.ML)"
   echo "    -g BOOL      generate session graph image for document (default false)"
   echo "    -i BOOL      generate HTML and graph browser information (default false)"
   echo "    -m MODE      add print mode for output"
@@ -63,6 +64,7 @@
 BUILD=""
 COMPRESS=true
 DOCUMENT=false
+ROOT_FILE=ROOT.ML
 DOCUMENT_GRAPH=false
 INFO=false
 MODES=""
@@ -74,7 +76,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:P:bc:d:g:i:m:p:rs:v:" OPT
+  while getopts "D:P:bc:d:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       D)
@@ -93,6 +95,9 @@
       d)
         DOCUMENT="$OPTARG"
         ;;
+      f)
+        ROOT_FILE="$OPTARG"
+        ;;
       g)
         check_bool "$OPTARG"
         DOCUMENT_GRAPH="$OPTARG"
@@ -189,7 +194,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
+    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -198,7 +203,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
+    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r 9e12b5443e7f -r f856f4f3258f src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Oct 28 17:11:51 2004 +0200
+++ b/src/Pure/Isar/session.ML	Thu Oct 28 19:40:22 2004 +0200
@@ -9,7 +9,7 @@
 sig
   val name: unit -> string
   val welcome: unit -> string
-  val use_dir: bool -> string list -> bool -> bool -> string -> bool -> string
+  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string
     -> string -> string -> string -> int -> bool -> unit
   val finish: unit -> unit
 end;
@@ -67,7 +67,9 @@
 
 (* use_dir *)
 
+(*
 val root_file = ThyLoad.ml_path "ROOT";
+*)
 
 fun get_rpath rpath_str =
   (if rpath_str = "" then () else
@@ -77,13 +79,13 @@
        rpath := Some (Url.unpack rpath_str);
    (!rpath, rpath_str <> ""));
 
-fun use_dir build modes reset info doc doc_graph parent name dump rpath_str level verbose =
+fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose =
   Library.setmp print_mode (modes @ ! print_mode)
     (Library.setmp Proofterm.proofs level (fn () =>
       (init reset parent name;
        Present.init build info doc doc_graph (path ()) name
          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
-       File.use root_file;
+       File.use (Path.basic root_file);
        finish ()))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);