src/Pure/Thy/present.ML
changeset 48445 cb4136e4cabf
parent 44986 6f27ecf2a951
child 48516 c5d0f19ef7cb
     1.1 --- a/src/Pure/Thy/present.ML	Mon Jul 23 14:18:28 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Jul 23 15:05:05 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4     path: string, parents: string list} list -> Path.T -> unit
     1.5    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     1.6     path: string, parents: string list} list -> unit
     1.7 -  val init: bool -> bool -> string -> bool -> string list -> string list ->
     1.8 +  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     1.9      string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
    1.10      theory list -> unit  (*not thread-safe!*)
    1.11    val finish: unit -> unit  (*not thread-safe!*)
    1.12 @@ -34,8 +34,6 @@
    1.13  
    1.14  (** paths **)
    1.15  
    1.16 -val output_path = Path.variable "ISABELLE_BROWSER_INFO";
    1.17 -
    1.18  val tex_ext = Path.ext "tex";
    1.19  val tex_path = tex_ext o Path.basic;
    1.20  val html_ext = Path.ext "html";
    1.21 @@ -275,7 +273,7 @@
    1.22  
    1.23  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    1.24  
    1.25 -fun init build info doc doc_graph doc_variants path name dump_prefix
    1.26 +fun init build info info_path doc doc_graph doc_variants path name dump_prefix
    1.27      (remote_path, first_time) verbose thys =
    1.28    if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
    1.29      (browser_info := empty_browser_info; session_info := NONE)
    1.30 @@ -284,7 +282,7 @@
    1.31        val parent_name = name_of_session (take (length path - 1) path);
    1.32        val session_name = name_of_session path;
    1.33        val sess_prefix = Path.make path;
    1.34 -      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
    1.35 +      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
    1.36  
    1.37        val documents =
    1.38          if doc = "" then []