build option enables most basic browser info (for proper recording of session);
authorwenzelm
Tue, 23 Oct 2001 22:54:01 +0200
changeset 11911 6533ceee4cd7
parent 11910 8b8923bfc259
child 11912 d1b341c3aabc
build option enables most basic browser info (for proper recording of session);
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Oct 23 22:53:08 2001 +0200
+++ b/src/Pure/Thy/present.ML	Tue Oct 23 22:54:01 2001 +0200
@@ -17,7 +17,7 @@
   include BASIC_PRESENT
   val write_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> Path.T -> unit
-  val init: bool -> string -> bool -> string list -> string -> Path.T option
+  val init: bool -> bool -> string -> bool -> string list -> string -> Path.T option
     -> Url.T option * bool -> bool -> unit
   val finish: unit -> unit
   val init_theory: string -> unit
@@ -272,8 +272,8 @@
      ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
 
 
-fun init info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
-  if not info andalso doc = "" andalso is_none doc_prefix2 then
+fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose =
+  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
     (browser_info := empty_browser_info; session_info := None)
   else
     let