# HG changeset patch
# User wenzelm
# Date 1343048705 -7200
# Node ID cb4136e4cabfadb3e81bad696e649c74377f6eee
# Parent  c8c7b2b388d1851834f5e834d0789dbed3bd08e0
pass ISABELLE_BROWSER_INFO as explicit argument;

diff -r c8c7b2b388d1 -r cb4136e4cabf lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Jul 23 14:18:28 2012 +0200
+++ b/lib/Tools/usedir	Mon Jul 23 15:05:05 2012 +0200
@@ -241,7 +241,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -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;" \
+    -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;" \
     -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -250,7 +250,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -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();" \
+    -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();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r c8c7b2b388d1 -r cb4136e4cabf src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Jul 23 14:18:28 2012 +0200
+++ b/src/Pure/System/session.ML	Mon Jul 23 15:05:05 2012 +0200
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val init: bool -> string -> string -> unit
-  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
   val finish: unit -> unit
@@ -94,12 +94,12 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
-fun use_dir item root build modes reset info doc doc_graph doc_variants parent
+fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
      (init reset parent name;
-      Present.init build info doc doc_graph doc_variants (path ()) name
+      Present.init build info info_path doc doc_graph doc_variants (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
       if timing then
         let
diff -r c8c7b2b388d1 -r cb4136e4cabf src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jul 23 14:18:28 2012 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jul 23 15:05:05 2012 +0200
@@ -17,7 +17,7 @@
    path: string, parents: string list} list -> Path.T -> unit
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
-  val init: bool -> bool -> string -> bool -> string list -> string list ->
+  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
@@ -34,8 +34,6 @@
 
 (** paths **)
 
-val output_path = Path.variable "ISABELLE_BROWSER_INFO";
-
 val tex_ext = Path.ext "tex";
 val tex_path = tex_ext o Path.basic;
 val html_ext = Path.ext "html";
@@ -275,7 +273,7 @@
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info doc doc_graph doc_variants path name dump_prefix
+fun init build info info_path doc doc_graph doc_variants path name dump_prefix
     (remote_path, first_time) verbose thys =
   if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
     (browser_info := empty_browser_info; session_info := NONE)
@@ -284,7 +282,7 @@
       val parent_name = name_of_session (take (length path - 1) path);
       val session_name = name_of_session path;
       val sess_prefix = Path.make path;
-      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
+      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
 
       val documents =
         if doc = "" then []