1.1 --- a/lib/Tools/usedir	Mon Jul 23 14:18:28 2012 +0200
     1.2 +++ b/lib/Tools/usedir	Mon Jul 23 15:05:05 2012 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4    LOG="$LOGDIR/$ITEM"
     1.5  
     1.6    "$ISABELLE_PROCESS" \
     1.7 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
     1.8 +    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
     1.9      -q -w $LOGIC $NAME > "$LOG"
    1.10    RC="$?"
    1.11  else
    1.12 @@ -250,7 +250,7 @@
    1.13    LOG="$LOGDIR/$ITEM"
    1.14  
    1.15    "$ISABELLE_PROCESS" \
    1.16 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
    1.17 +    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
    1.18      -r -q "$LOGIC" > "$LOG"
    1.19    RC="$?"
    1.20    cd ..

     2.1 --- a/src/Pure/System/session.ML	Mon Jul 23 14:18:28 2012 +0200
     2.2 +++ b/src/Pure/System/session.ML	Mon Jul 23 15:05:05 2012 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val name: unit -> string
     2.5    val welcome: unit -> string
     2.6    val init: bool -> string -> string -> unit
     2.7 -  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
     2.8 +  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     2.9      string -> bool -> string list -> string -> string -> bool * string ->
    2.10      string -> int -> bool -> bool -> int -> int -> int -> int -> unit
    2.11    val finish: unit -> unit
    2.12 @@ -94,12 +94,12 @@
    2.13  fun dumping (_, "") = NONE
    2.14    | dumping (cp, path) = SOME (cp, Path.explode path);
    2.15  
    2.16 -fun use_dir item root build modes reset info doc doc_graph doc_variants parent
    2.17 +fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    2.18      name dump rpath level timing verbose max_threads trace_threads
    2.19      parallel_proofs parallel_proofs_threshold =
    2.20    ((fn () =>
    2.21       (init reset parent name;
    2.22 -      Present.init build info doc doc_graph doc_variants (path ()) name
    2.23 +      Present.init build info info_path doc doc_graph doc_variants (path ()) name
    2.24          (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
    2.25        if timing then
    2.26          let

     3.1 --- a/src/Pure/Thy/present.ML	Mon Jul 23 14:18:28 2012 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Mon Jul 23 15:05:05 2012 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4     path: string, parents: string list} list -> Path.T -> unit
     3.5    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     3.6     path: string, parents: string list} list -> unit
     3.7 -  val init: bool -> bool -> string -> bool -> string list -> string list ->
     3.8 +  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     3.9      string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
    3.10      theory list -> unit  (*not thread-safe!*)
    3.11    val finish: unit -> unit  (*not thread-safe!*)
    3.12 @@ -34,8 +34,6 @@
    3.13  
    3.14  (** paths **)
    3.15  
    3.16 -val output_path = Path.variable "ISABELLE_BROWSER_INFO";
    3.17 -
    3.18  val tex_ext = Path.ext "tex";
    3.19  val tex_path = tex_ext o Path.basic;
    3.20  val html_ext = Path.ext "html";
    3.21 @@ -275,7 +273,7 @@
    3.22  
    3.23  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    3.24  
    3.25 -fun init build info doc doc_graph doc_variants path name dump_prefix
    3.26 +fun init build info info_path doc doc_graph doc_variants path name dump_prefix
    3.27      (remote_path, first_time) verbose thys =
    3.28    if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
    3.29      (browser_info := empty_browser_info; session_info := NONE)
    3.30 @@ -284,7 +282,7 @@
    3.31        val parent_name = name_of_session (take (length path - 1) path);
    3.32        val session_name = name_of_session path;
    3.33        val sess_prefix = Path.make path;
    3.34 -      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
    3.35 +      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
    3.36  
    3.37        val documents =
    3.38          if doc = "" then []