discontinued "isabelle usedir" option -r (reset session path);
authorwenzelm
Tue Mar 12 16:47:24 2013 +0100 (2013-03-12)
changeset 513996ac3c29a300e
parent 51398 c3d02b3518c2
child 51400 96361e8f0a54
discontinued "isabelle usedir" option -r (reset session path);
simplified internal session identification: chapter / name;
clarified chapter index (of sessions) vs. session index (of theories);
discontinued "up" links, for improved modularity also wrt. partial browser_info (users can use "back" within the browser);
removed obsolete session parent_path;
NEWS
src/Pure/System/session.ML
src/Pure/Thy/html.ML
src/Pure/Thy/html.scala
src/Pure/Thy/present.ML
src/Pure/Thy/present.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Mon Mar 11 14:25:14 2013 +0100
     1.2 +++ b/NEWS	Tue Mar 12 16:47:24 2013 +0100
     1.3 @@ -63,9 +63,9 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 -* Discontinued "isabelle usedir" option -P (remote path).  Note that
     1.8 -usedir is legacy and superseded by "isabelle build" since
     1.9 -Isabelle2013.
    1.10 +* Discontinued "isabelle usedir" option -P (remote path) and -r (reset
    1.11 +session path).  Note that usedir is legacy and superseded by "isabelle
    1.12 +build" since Isabelle2013.
    1.13  
    1.14  
    1.15  
     2.1 --- a/src/Pure/System/session.ML	Mon Mar 11 14:25:14 2013 +0100
     2.2 +++ b/src/Pure/System/session.ML	Tue Mar 12 16:47:24 2013 +0100
     2.3 @@ -1,18 +1,16 @@
     2.4  (*  Title:      Pure/System/session.ML
     2.5      Author:     Markus Wenzel, TU Muenchen
     2.6  
     2.7 -Session management -- maintain state of logic images.
     2.8 +Session management -- internal state of logic images.
     2.9  *)
    2.10  
    2.11  signature SESSION =
    2.12  sig
    2.13 -  val id: unit -> string list
    2.14    val name: unit -> string
    2.15 -  val path: unit -> string list
    2.16    val welcome: unit -> string
    2.17 +  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    2.18 +    string -> string * string -> bool * string -> bool -> unit
    2.19    val finish: unit -> unit
    2.20 -  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
    2.21 -    string -> string -> bool * string -> bool -> unit
    2.22    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    2.23    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    2.24      string -> bool -> string list -> string -> string -> bool * string ->
    2.25 @@ -24,21 +22,10 @@
    2.26  
    2.27  (* session state *)
    2.28  
    2.29 -val session = Unsynchronized.ref ([Context.PureN]: string list);
    2.30 +val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
    2.31  val session_finished = Unsynchronized.ref false;
    2.32  
    2.33 -fun id () = ! session;
    2.34 -fun name () = "Isabelle/" ^ List.last (! session);
    2.35 -
    2.36 -
    2.37 -(* access path *)
    2.38 -
    2.39 -val session_path = Unsynchronized.ref ([]: string list);
    2.40 -
    2.41 -fun path () = ! session_path;
    2.42 -
    2.43 -
    2.44 -(* welcome *)
    2.45 +fun name () = "Isabelle/" ^ #name (! session);
    2.46  
    2.47  fun welcome () =
    2.48    if Distribution.is_official then
    2.49 @@ -46,22 +33,21 @@
    2.50    else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
    2.51  
    2.52  
    2.53 -(* add_path *)
    2.54 +(* init *)
    2.55  
    2.56 -fun add_path reset s =
    2.57 -  let val sess = ! session @ [s] in
    2.58 -    (case duplicates (op =) sess of
    2.59 -      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    2.60 -    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
    2.61 -  end;
    2.62 -
    2.63 -
    2.64 -(* init_name *)
    2.65 -
    2.66 -fun init_name reset parent name =
    2.67 -  if not (member (op =) (! session) parent) orelse not (! session_finished) then
    2.68 +fun init build info info_path doc doc_graph doc_output doc_variants
    2.69 +    parent (chapter, name) doc_dump verbose =
    2.70 +  if #name (! session) <> parent orelse not (! session_finished) then
    2.71      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    2.72 -  else (add_path reset name; session_finished := false);
    2.73 +  else
    2.74 +    let
    2.75 +      val _ = session := {chapter = chapter, name = name};
    2.76 +      val _ = session_finished := false;
    2.77 +    in
    2.78 +      Present.init build info info_path (if doc = "false" then "" else doc)
    2.79 +        doc_graph doc_output doc_variants (chapter, name)
    2.80 +        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    2.81 +    end;
    2.82  
    2.83  
    2.84  (* finish *)
    2.85 @@ -77,7 +63,7 @@
    2.86    session_finished := true);
    2.87  
    2.88  
    2.89 -(* use_dir *)
    2.90 +(* timing within ML *)
    2.91  
    2.92  fun with_timing name verbose f x =
    2.93    let
    2.94 @@ -99,21 +85,13 @@
    2.95        else ();
    2.96    in y end;
    2.97  
    2.98 -fun init build reset info info_path doc doc_graph doc_output doc_variants
    2.99 -    parent name doc_dump verbose =
   2.100 - (init_name reset parent name;
   2.101 -  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
   2.102 -    doc_variants (path ()) name doc_dump verbose
   2.103 -    (map Thy_Info.get_theory (Thy_Info.get_names ())));
   2.104  
   2.105 -local
   2.106 +(* use_dir *)
   2.107  
   2.108  fun read_variants strs =
   2.109    rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   2.110    |> filter_out (fn (_, s) => s = "-");
   2.111  
   2.112 -in
   2.113 -
   2.114  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
   2.115      name doc_dump rpath level timing verbose max_threads trace_threads
   2.116      parallel_proofs parallel_proofs_threshold =
   2.117 @@ -123,13 +101,15 @@
   2.118          Output.physical_stderr
   2.119            "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
   2.120        val _ =
   2.121 +        if not reset then ()
   2.122 +        else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n";
   2.123 +      val _ =
   2.124          if rpath = "" then ()
   2.125 -        else
   2.126 -          Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
   2.127 +        else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
   2.128  
   2.129        val _ =
   2.130 -        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
   2.131 -          doc_dump verbose;
   2.132 +        init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants)
   2.133 +          parent ("Unsorted", name) doc_dump verbose;
   2.134        val res1 = (use |> with_timing item timing |> Exn.capture) root;
   2.135        val res2 = Exn.capture finish ();
   2.136      in ignore (Par_Exn.release_all [res1, res2]) end)
   2.137 @@ -144,5 +124,3 @@
   2.138    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
   2.139  
   2.140  end;
   2.141 -
   2.142 -end;
     3.1 --- a/src/Pure/Thy/html.ML	Mon Mar 11 14:25:14 2013 +0100
     3.2 +++ b/src/Pure/Thy/html.ML	Tue Mar 12 16:47:24 2013 +0100
     3.3 @@ -22,12 +22,11 @@
     3.4    val verbatim: string -> text
     3.5    val begin_document: string -> text
     3.6    val end_document: text
     3.7 -  val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
     3.8 +  val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
     3.9    val applet_pages: string -> Url.T * string -> (string * string) list
    3.10    val theory_entry: Url.T * string -> text
    3.11 -  val session_entries: (Url.T * string) list -> text
    3.12    val theory_source: text -> text
    3.13 -  val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
    3.14 +  val begin_theory: string -> (Url.T option * string) list ->
    3.15      (Url.T * Url.T * bool) list -> text -> text
    3.16    val external_file: Url.T -> string -> text
    3.17  end;
    3.18 @@ -288,15 +287,11 @@
    3.19  
    3.20  val end_document = "\n</div>\n</body>\n</html>\n";
    3.21  
    3.22 -fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
    3.23 -val up_link = gen_link "Up";
    3.24 -val back_link = gen_link "Back";
    3.25 -
    3.26  
    3.27  (* session index *)
    3.28  
    3.29 -fun begin_index up (index_path, session) docs graph =
    3.30 -  begin_document ("Index of " ^ session) ^ up_link up ^
    3.31 +fun begin_session_index session docs graph =
    3.32 +  begin_document ("Session " ^ plain session) ^
    3.33    para ("View " ^ href_path graph "theory dependencies" ^
    3.34      implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
    3.35    "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
    3.36 @@ -304,6 +299,8 @@
    3.37  fun choice chs s = space_implode " " (map (fn (s', lnk) =>
    3.38    enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
    3.39  
    3.40 +fun back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name);
    3.41 +
    3.42  fun applet_pages session back =
    3.43    let
    3.44      val sizes =
    3.45 @@ -329,14 +326,7 @@
    3.46    in map applet_page sizes end;
    3.47  
    3.48  
    3.49 -fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
    3.50 -
    3.51 -val theory_entry = entry;
    3.52 -
    3.53 -fun session_entries [] = "</ul>"
    3.54 -  | session_entries es =
    3.55 -      "</ul>\n</div>\n<div class=\"sessions\">\n\
    3.56 -      \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
    3.57 +fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
    3.58  
    3.59  
    3.60  (* theory *)
    3.61 @@ -350,9 +340,8 @@
    3.62    fun file (href, path, loadit) =
    3.63      href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
    3.64  
    3.65 -  fun theory up A =
    3.66 -    begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
    3.67 -    command "theory" ^ " " ^ name A;
    3.68 +  fun theory A =
    3.69 +    begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A;
    3.70  
    3.71    fun imports Bs =
    3.72      keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
    3.73 @@ -360,8 +349,8 @@
    3.74    fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
    3.75  in
    3.76  
    3.77 -fun begin_theory up A Bs Ps body =
    3.78 -  theory up A ^ "<br/>\n" ^
    3.79 +fun begin_theory A Bs Ps body =
    3.80 +  theory A ^ "<br/>\n" ^
    3.81    imports Bs ^ "<br/>\n" ^
    3.82    (if null Ps then "" else uses Ps) ^
    3.83    body;
     4.1 --- a/src/Pure/Thy/html.scala	Mon Mar 11 14:25:14 2013 +0100
     4.2 +++ b/src/Pure/Thy/html.scala	Tue Mar 12 16:47:24 2013 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4  
     4.5  object HTML
     4.6  {
     4.7 -  // encode text
     4.8 +  /* encode text */
     4.9  
    4.10    def encode(text: String): String =
    4.11    {
    4.12 @@ -29,7 +29,27 @@
    4.13    }
    4.14  
    4.15  
    4.16 -  // common markup elements
    4.17 +  /* document */
    4.18 +
    4.19 +  val end_document = "\n</div>\n</body>\n</html>\n"
    4.20 +
    4.21 +  def begin_document(title: String): String =
    4.22 +    "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
    4.23 +    "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
    4.24 +    "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
    4.25 +    "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
    4.26 +    "<head>\n" +
    4.27 +    "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
    4.28 +    "<title>" + encode(title) + "</title>\n" +
    4.29 +    "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
    4.30 +    "</head>\n" +
    4.31 +    "\n" +
    4.32 +    "<body>\n" +
    4.33 +    "<div class=\"head\">" +
    4.34 +    "<h1>" + encode(title) + "</h1>\n"
    4.35 +
    4.36 +
    4.37 +  /* common markup elements */
    4.38  
    4.39    def session_entry(name: String): String =
    4.40      XML.string_of_tree(
    4.41 @@ -37,11 +57,11 @@
    4.42          List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
    4.43            List(XML.Text(name)))))) + "\n"
    4.44  
    4.45 -  def session_entries(names: List[String]): String =
    4.46 -    if (names.isEmpty) "</ul>"
    4.47 -    else
    4.48 -      "</ul>\n</div>\n<div class=\"sessions\">\n" +
    4.49 -      "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
    4.50 -
    4.51 -  val end_document = "\n</div>\n</body>\n</html>\n"
    4.52 +  def chapter_index(chapter: String, sessions: List[String]): String =
    4.53 +  {
    4.54 +    begin_document("Isabelle/" + chapter + " sessions") +
    4.55 +      (if (sessions.isEmpty) ""
    4.56 +       else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
    4.57 +    end_document
    4.58 +  }
    4.59  }
     5.1 --- a/src/Pure/Thy/present.ML	Mon Mar 11 14:25:14 2013 +0100
     5.2 +++ b/src/Pure/Thy/present.ML	Tue Mar 12 16:47:24 2013 +0100
     5.3 @@ -14,8 +14,8 @@
     5.4    include BASIC_PRESENT
     5.5    val session_name: theory -> string
     5.6    val read_variant: string -> string * string
     5.7 -  val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     5.8 -    string list -> string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
     5.9 +  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    5.10 +    string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
    5.11    val finish: unit -> unit  (*not thread-safe!*)
    5.12    val init_theory: string -> unit
    5.13    val theory_source: string -> (unit -> HTML.text) -> unit
    5.14 @@ -44,16 +44,6 @@
    5.15  val graph_pdf_path = Path.basic "session_graph.pdf";
    5.16  val graph_eps_path = Path.basic "session_graph.eps";
    5.17  
    5.18 -val session_path = Path.basic ".session";
    5.19 -val session_entries_path = Path.explode ".session/entries";
    5.20 -val pre_index_path = Path.explode ".session/pre-index";
    5.21 -
    5.22 -fun mk_rel_path [] ys = Path.make ys
    5.23 -  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
    5.24 -  | mk_rel_path (ps as x :: xs) (qs as y :: ys) =
    5.25 -      if x = y then mk_rel_path xs ys
    5.26 -      else Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    5.27 -
    5.28  fun show_path path = Path.implode (Path.append (File.pwd ()) path);
    5.29  
    5.30  
    5.31 @@ -62,34 +52,41 @@
    5.32  
    5.33  structure Browser_Info = Theory_Data
    5.34  (
    5.35 -  type T = {name: string, session: string list};
    5.36 -  val empty = {name = "", session = []}: T;
    5.37 +  type T = {chapter: string, name: string};
    5.38 +  val empty = {chapter = "Unsorted", name = "Unknown"}: T;  (* FIXME !? *)
    5.39    fun extend _ = empty;
    5.40    fun merge _ = empty;
    5.41  );
    5.42  
    5.43 -val put_info = Browser_Info.put;
    5.44 -val get_info = Browser_Info.get;
    5.45 -val session_name = #name o get_info;
    5.46 +val session_name = #name o Browser_Info.get;
    5.47 +val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
    5.48  
    5.49  
    5.50  
    5.51  (** graphs **)
    5.52  
    5.53  fun ID_of sess s = space_implode "/" (sess @ [s]);
    5.54 -fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
    5.55 +fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
    5.56  
    5.57 +fun theory_link curr_chapter thy =
    5.58 +  let
    5.59 +    val chapter = #chapter (Browser_Info.get thy);
    5.60 +    val thy_html = html_path (Context.theory_name thy);
    5.61 +  in
    5.62 +    if curr_chapter = chapter then thy_html
    5.63 +    else Path.appends [Path.parent, Path.basic chapter, thy_html]
    5.64 +  end;
    5.65  
    5.66  (*retrieve graph data from initial collection of theories*)
    5.67 -fun init_graph curr_sess = rev o map (fn thy =>
    5.68 +fun init_graph curr_chapter = rev o map (fn thy =>
    5.69    let
    5.70 -    val name = Context.theory_name thy;
    5.71 -    val {name = sess_name, session} = get_info thy;
    5.72 +    val {chapter, name = session_name} = Browser_Info.get thy;
    5.73 +    val thy_name = Context.theory_name thy;
    5.74      val entry =
    5.75 -     {name = name, ID = ID_of session name, dir = sess_name,
    5.76 -      path =
    5.77 -        if null session then ""
    5.78 -        else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
    5.79 +     {name = thy_name,
    5.80 +      ID = ID_of [chapter, session_name] thy_name,
    5.81 +      dir = session_name,
    5.82 +      path = Path.implode (theory_link curr_chapter thy),
    5.83        unfold = false,
    5.84        parents = map ID_of_thy (Theory.parents_of thy),
    5.85        content = []};
    5.86 @@ -127,8 +124,8 @@
    5.87  
    5.88  val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
    5.89  
    5.90 -fun init_browser_info curr_sess thys = make_browser_info
    5.91 -  (Symtab.empty, [], [], [], init_graph curr_sess thys);
    5.92 +fun init_browser_info chapter thys =
    5.93 +  make_browser_info (Symtab.empty, [], [], [], init_graph chapter thys);
    5.94  
    5.95  fun map_browser_info f {theories, files, tex_index, html_index, graph} =
    5.96    make_browser_info (f (theories, files, tex_index, html_index, graph));
    5.97 @@ -186,16 +183,16 @@
    5.98  (* session_info *)
    5.99  
   5.100  type session_info =
   5.101 -  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   5.102 +  {name: string, chapter: string, info_path: Path.T,
   5.103      info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
   5.104      documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
   5.105      readme: Path.T option};
   5.106  
   5.107  fun make_session_info
   5.108 -  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
   5.109 +  (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
   5.110      documents, doc_dump, verbose, readme) =
   5.111 -  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   5.112 -    info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
   5.113 +  {name = name, chapter = chapter, info_path = info_path, info = info,
   5.114 +    doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
   5.115      documents = documents, doc_dump = doc_dump, verbose = verbose,
   5.116      readme = readme}: session_info;
   5.117  
   5.118 @@ -204,36 +201,12 @@
   5.119  
   5.120  val session_info = Unsynchronized.ref (NONE: session_info option);
   5.121  
   5.122 -fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
   5.123 +fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
   5.124  
   5.125  
   5.126  
   5.127  (** document preparation **)
   5.128  
   5.129 -(* maintain session index *)
   5.130 -
   5.131 -val session_entries =
   5.132 -  HTML.session_entries o
   5.133 -    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
   5.134 -
   5.135 -fun get_entries dir =
   5.136 -  split_lines (File.read (Path.append dir session_entries_path));
   5.137 -
   5.138 -fun put_entries entries dir =
   5.139 -  File.write (Path.append dir session_entries_path) (cat_lines entries);
   5.140 -
   5.141 -
   5.142 -fun create_index dir =
   5.143 -  File.read (Path.append dir pre_index_path) ^
   5.144 -    session_entries (get_entries dir) ^ HTML.end_document
   5.145 -  |> File.write (Path.append dir index_path);
   5.146 -
   5.147 -fun update_index dir name =
   5.148 -  (case try get_entries dir of
   5.149 -    NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
   5.150 -  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
   5.151 -
   5.152 -
   5.153  (* document variants *)
   5.154  
   5.155  fun read_variant str =
   5.156 @@ -245,19 +218,14 @@
   5.157  
   5.158  (* init session *)
   5.159  
   5.160 -fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
   5.161 -
   5.162 -fun init build info info_path doc doc_graph document_output doc_variants path name
   5.163 -    (doc_dump as (_, dump_prefix)) verbose thys =
   5.164 +fun init build info info_path doc doc_graph document_output doc_variants
   5.165 +    (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys =
   5.166    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
   5.167      (browser_info := empty_browser_info; session_info := NONE)
   5.168    else
   5.169      let
   5.170 -      val parent_name = name_of_session (take (length path - 1) path);
   5.171 -      val session_name = name_of_session path;
   5.172 -      val sess_prefix = Path.make path;
   5.173 -      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
   5.174 -      val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
   5.175 +      val doc_output =
   5.176 +        if document_output = "" then NONE else SOME (Path.explode document_output);
   5.177  
   5.178        val documents =
   5.179          if doc = "" then []
   5.180 @@ -266,8 +234,6 @@
   5.181             else (); [])
   5.182          else doc_variants;
   5.183  
   5.184 -      val parent_index_path = Path.append Path.parent index_path;
   5.185 -      val index_up_lnk = Url.File parent_index_path;
   5.186        val readme =
   5.187          if File.exists readme_html_path then SOME readme_html_path
   5.188          else if File.exists readme_path then SOME readme_path
   5.189 @@ -276,13 +242,13 @@
   5.190        val docs =
   5.191          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
   5.192            map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
   5.193 -      val index_text = HTML.begin_index (index_up_lnk, parent_name)
   5.194 -        (Url.File index_path, session_name) docs (Url.explode "medium.html");
   5.195 +      val index_text =  (* FIXME move to finish!? *)
   5.196 +        HTML.begin_session_index name docs (Url.explode "medium.html");
   5.197      in
   5.198        session_info :=
   5.199 -        SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
   5.200 +        SOME (make_session_info (name, chapter, info_path, info, doc,
   5.201            doc_graph, doc_output, documents, doc_dump, verbose, readme));
   5.202 -      browser_info := init_browser_info path thys;
   5.203 +      browser_info := init_browser_info chapter thys;
   5.204        add_html_index (0, index_text)
   5.205      end;
   5.206  
   5.207 @@ -331,15 +297,18 @@
   5.208  
   5.209  
   5.210  fun finish () =
   5.211 -  session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
   5.212 -    documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
   5.213 +  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
   5.214 +    documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
   5.215    let
   5.216      val {theories, files, tex_index, html_index, graph} = ! browser_info;
   5.217      val thys = Symtab.dest theories;
   5.218 -    val parent_html_prefix = Path.append html_prefix Path.parent;
   5.219 +
   5.220 +    val chapter_prefix = Path.append info_path (Path.basic chapter);
   5.221 +    val session_prefix = Path.append chapter_prefix (Path.basic name);
   5.222  
   5.223      fun finish_html (a, {html, ...}: theory_info) =
   5.224 -      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
   5.225 +      File.write_buffer (Path.append session_prefix (html_path a))
   5.226 +        (Buffer.add HTML.end_document html);
   5.227  
   5.228      val sorted_graph = sorted_index graph;
   5.229      val opt_graphs =
   5.230 @@ -349,21 +318,19 @@
   5.231  
   5.232      val _ =
   5.233        if info then
   5.234 -       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
   5.235 -        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
   5.236 -        File.write (Path.append html_prefix session_entries_path) "";
   5.237 -        create_index html_prefix;
   5.238 -        if length path > 1 then update_index parent_html_prefix name else ();
   5.239 -        (case readme of NONE => () | SOME path => File.copy path html_prefix);
   5.240 -        Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph;
   5.241 +       (Isabelle_System.mkdirs session_prefix;
   5.242 +        File.write_buffer (Path.append session_prefix index_path)
   5.243 +          (index_buffer html_index |> Buffer.add HTML.end_document);
   5.244 +        (case readme of NONE => () | SOME path => File.copy path session_prefix);
   5.245 +        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
   5.246          Isabelle_System.isabelle_tool "browser" "-b";
   5.247 -        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
   5.248 -        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
   5.249 +        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
   5.250 +        List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
   5.251            (HTML.applet_pages name (Url.File index_path, name));
   5.252 -        File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
   5.253 +        File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
   5.254          List.app finish_html thys;
   5.255          List.app (uncurry File.write) files;
   5.256 -        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
   5.257 +        if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
   5.258          else ())
   5.259        else ();
   5.260  
   5.261 @@ -409,7 +376,7 @@
   5.262  
   5.263      val jobs =
   5.264        (if info orelse is_none doc_output then
   5.265 -        map (document_job html_prefix true) documents
   5.266 +        map (document_job session_prefix true) documents
   5.267         else []) @
   5.268        (case doc_output of
   5.269          NONE => []
   5.270 @@ -424,30 +391,23 @@
   5.271  
   5.272  (* theory elements *)
   5.273  
   5.274 -fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
   5.275 +fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info);
   5.276  
   5.277  fun theory_source name mk_text =
   5.278 -  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
   5.279 +  with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
   5.280  
   5.281  fun theory_output name s =
   5.282 -  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   5.283 +  with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s));
   5.284  
   5.285  
   5.286 -fun parent_link curr_session thy =
   5.287 +fun begin_theory update_time dir thy =
   5.288 +    with_session_info thy (fn {name = session_name, chapter, info_path, ...} =>
   5.289    let
   5.290 -    val {name = _, session} = get_info thy;
   5.291 -    val name = Context.theory_name thy;
   5.292 -    val link =
   5.293 -      if null session then NONE
   5.294 -      else SOME (Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   5.295 -  in (link, name) end;
   5.296 -
   5.297 -fun begin_theory update_time dir thy =
   5.298 -    session_default thy (fn {name = sess_name, session, path, html_prefix, ...} =>
   5.299 -  let
   5.300 +    val path = [chapter, session_name];
   5.301      val name = Context.theory_name thy;
   5.302      val parents = Theory.parents_of thy;
   5.303 -    val parent_specs = map (parent_link path) parents;
   5.304 +    val parent_specs = parents |> map (fn parent =>
   5.305 +      (SOME (Url.File (theory_link chapter parent)), name));
   5.306  
   5.307      val files = [];  (* FIXME *)
   5.308      val files_html = files |> map (fn (raw_path, loadit) =>
   5.309 @@ -455,18 +415,19 @@
   5.310          val path = File.check_file (File.full_path dir raw_path);
   5.311          val base = Path.base path;
   5.312          val base_html = html_ext base;
   5.313 -        val _ = add_file (Path.append html_prefix base_html,
   5.314 -          HTML.external_file (Url.File base) (File.read path));
   5.315 +        (* FIXME retain file path!? *)
   5.316 +        val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name];
   5.317 +        val _ =
   5.318 +          add_file (Path.append session_prefix base_html,
   5.319 +            HTML.external_file (Url.File base) (File.read path));
   5.320        in (Url.File base_html, Url.File raw_path, loadit) end);
   5.321  
   5.322      fun prep_html_source (tex_source, html_source, html) =
   5.323 -      let
   5.324 -        val txt = HTML.begin_theory (Url.File index_path, session)
   5.325 -          name parent_specs files_html (Buffer.content html_source)
   5.326 +      let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source)
   5.327        in (tex_source, Buffer.empty, Buffer.add txt html) end;
   5.328  
   5.329      val entry =
   5.330 -     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
   5.331 +     {name = name, ID = ID_of path name, dir = session_name, unfold = true,
   5.332        path = Path.implode (html_path name),
   5.333        parents = map ID_of_thy parents,
   5.334        content = []};
   5.335 @@ -475,7 +436,7 @@
   5.336      add_graph_entry (update_time, entry);
   5.337      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
   5.338      add_tex_index (update_time, Latex.theory_entry name);
   5.339 -    put_info {name = sess_name, session = path} thy
   5.340 +    Browser_Info.put {chapter = chapter, name = session_name} thy
   5.341    end);
   5.342  
   5.343  
     6.1 --- a/src/Pure/Thy/present.scala	Mon Mar 11 14:25:14 2013 +0100
     6.2 +++ b/src/Pure/Thy/present.scala	Tue Mar 12 16:47:24 2013 +0100
     6.3 @@ -9,33 +9,29 @@
     6.4  
     6.5  object Present
     6.6  {
     6.7 -  /* maintain session index -- NOT thread-safe */
     6.8 +  /* maintain chapter index -- NOT thread-safe */
     6.9  
    6.10    private val index_path = Path.basic("index.html")
    6.11 -  private val session_entries_path = Path.explode(".session/entries")
    6.12 -  private val pre_index_path = Path.explode(".session/pre-index")
    6.13 +  private val sessions_path = Path.basic(".sessions")
    6.14  
    6.15 -  private def get_entries(dir: Path): List[String] =
    6.16 -    split_lines(File.read(dir + session_entries_path))
    6.17 +  private def read_sessions(dir: Path): List[String] =
    6.18 +    split_lines(File.read(dir + sessions_path))
    6.19  
    6.20 -  private def put_entries(entries: List[String], dir: Path): Unit =
    6.21 -    File.write(dir + session_entries_path, cat_lines(entries))
    6.22 +  private def write_sessions(dir: Path, sessions: List[String]): Unit =
    6.23 +    File.write(dir + sessions_path, cat_lines(sessions))
    6.24  
    6.25 -  def create_index(dir: Path): Unit =
    6.26 -    File.write(dir + index_path,
    6.27 -      File.read(dir + pre_index_path) +
    6.28 -      HTML.session_entries(get_entries(dir)) +
    6.29 -      HTML.end_document)
    6.30 +  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[String]): Unit =
    6.31 +  {
    6.32 +    val dir = info_path + Path.basic(chapter)
    6.33 +    Isabelle_System.mkdirs(dir)
    6.34  
    6.35 -  def update_index(dir: Path, names: List[String]): Unit =
    6.36 -    try {
    6.37 -      put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
    6.38 -      create_index(dir)
    6.39 -    }
    6.40 -    catch {
    6.41 -      case ERROR(msg) =>
    6.42 -        java.lang.System.err.println(
    6.43 -          "### " + msg + "\n### Browser info: failed to update session index of " + dir)
    6.44 -    }
    6.45 +    val sessions0 =
    6.46 +      try { split_lines(File.read(dir + sessions_path)) }
    6.47 +      catch { case ERROR(_) => Nil }
    6.48 +
    6.49 +    val sessions = sessions0.filterNot(new_sessions.contains) ::: new_sessions
    6.50 +    write_sessions(dir, sessions)
    6.51 +    File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    6.52 +  }
    6.53  }
    6.54  
     7.1 --- a/src/Pure/Tools/build.ML	Mon Mar 11 14:25:14 2013 +0100
     7.2 +++ b/src/Pure/Tools/build.ML	Tue Mar 12 16:47:24 2013 +0100
     7.3 @@ -109,11 +109,12 @@
     7.4  fun build args_file = Command_Line.tool (fn () =>
     7.5      let
     7.6        val (command_timings, (do_output, (options, (verbose, (browser_info,
     7.7 -          (parent_name, (name, theories))))))) =
     7.8 +          (parent_name, (chapter, (name, theories)))))))) =
     7.9          File.read (Path.explode args_file) |> YXML.parse_body |>
    7.10            let open XML.Decode in
    7.11              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    7.12 -              (pair string (pair string ((list (pair Options.decode (list string))))))))))
    7.13 +              (pair string (pair string (pair string
    7.14 +                ((list (pair Options.decode (list string)))))))))))
    7.15            end;
    7.16  
    7.17        val document_variants =
    7.18 @@ -125,17 +126,14 @@
    7.19  
    7.20        val _ = writeln ("\fSession.name = " ^ name);
    7.21        val _ =
    7.22 -        (case Session.path () of
    7.23 -          [] => ()
    7.24 -        | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
    7.25 -      val _ =
    7.26 -        Session.init do_output false
    7.27 -          (Options.bool options "browser_info") browser_info
    7.28 +        Session.init do_output
    7.29 +          (Options.bool options "browser_info")
    7.30 +          (Path.explode browser_info)
    7.31            (Options.string options "document")
    7.32            (Options.bool options "document_graph")
    7.33            (Options.string options "document_output")
    7.34            document_variants
    7.35 -          parent_name name
    7.36 +          parent_name (chapter, name)
    7.37            (false, "")
    7.38            verbose;
    7.39  
     8.1 --- a/src/Pure/Tools/build.scala	Mon Mar 11 14:25:14 2013 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 12 16:47:24 2013 +0100
     8.3 @@ -497,9 +497,10 @@
     8.4          {
     8.5            import XML.Encode._
     8.6                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
     8.7 -                pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
     8.8 +                pair(string, pair(string, pair(string,
     8.9 +                  list(pair(Options.encode, list(Path.encode)))))))))))(
    8.10                (command_timings, (do_output, (info.options, (verbose, (browser_info,
    8.11 -                (parent, (name, info.theories))))))))
    8.12 +                (parent, (info.chapter, (name, info.theories)))))))))
    8.13          }))
    8.14  
    8.15      private val env =
    8.16 @@ -595,7 +596,6 @@
    8.17    private def log_gz(name: String): Path = log(name).ext("gz")
    8.18  
    8.19    private val SESSION_NAME = "\fSession.name = "
    8.20 -  private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    8.21  
    8.22  
    8.23    sealed case class Log_Info(
    8.24 @@ -754,7 +754,7 @@
    8.25      }
    8.26  
    8.27      // scheduler loop
    8.28 -    case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
    8.29 +    case class Result(current: Boolean, heap: String, rc: Int)
    8.30  
    8.31      def sleep(): Unit = Thread.sleep(500)
    8.32  
    8.33 @@ -775,7 +775,7 @@
    8.34              val res = job.join
    8.35              progress.echo(res.err)
    8.36  
    8.37 -            val (parent_path, heap) =
    8.38 +            val heap =
    8.39                if (res.rc == 0) {
    8.40                  (output_dir + log(name)).file.delete
    8.41  
    8.42 @@ -784,13 +784,7 @@
    8.43                  File.write_gzip(output_dir + log_gz(name),
    8.44                    sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
    8.45  
    8.46 -                val parent_path =
    8.47 -                  if (job.info.options.bool("browser_info"))
    8.48 -                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH))
    8.49 -                      .map(_.substring(SESSION_PARENT_PATH.length))
    8.50 -                  else None
    8.51 -
    8.52 -                (parent_path, heap)
    8.53 +                heap
    8.54                }
    8.55                else {
    8.56                  (output_dir + Path.basic(name)).file.delete
    8.57 @@ -805,10 +799,10 @@
    8.58                    progress.echo("\n" + cat_lines(tail))
    8.59                  }
    8.60  
    8.61 -                (None, no_heap)
    8.62 +                no_heap
    8.63                }
    8.64              loop(pending - name, running - name,
    8.65 -              results + (name -> Result(false, parent_path, heap, res.rc)))
    8.66 +              results + (name -> Result(false, heap, res.rc)))
    8.67              //}}}
    8.68            case None if (running.size < (max_jobs max 1)) =>
    8.69              //{{{ check/start next job
    8.70 @@ -816,7 +810,7 @@
    8.71                case Some((name, info)) =>
    8.72                  val parent_result =
    8.73                    info.parent match {
    8.74 -                    case None => Result(true, None, no_heap, 0)
    8.75 +                    case None => Result(true, no_heap, 0)
    8.76                      case Some(parent) => results(parent)
    8.77                    }
    8.78                  val output = output_dir + Path.basic(name)
    8.79 @@ -839,10 +833,10 @@
    8.80                  val all_current = current && parent_result.current
    8.81  
    8.82                  if (all_current)
    8.83 -                  loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
    8.84 +                  loop(pending - name, running, results + (name -> Result(true, heap, 0)))
    8.85                  else if (no_build) {
    8.86                    if (verbose) progress.echo("Skipping " + name + " ...")
    8.87 -                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
    8.88 +                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
    8.89                  }
    8.90                  else if (parent_result.rc == 0 && !progress.stopped) {
    8.91                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    8.92 @@ -853,7 +847,7 @@
    8.93                  }
    8.94                  else {
    8.95                    progress.echo(name + " CANCELLED")
    8.96 -                  loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
    8.97 +                  loop(pending - name, running, results + (name -> Result(false, heap, 1)))
    8.98                  }
    8.99                case None => sleep(); loop(pending, running, results)
   8.100              }
   8.101 @@ -874,11 +868,11 @@
   8.102        else loop(queue, Map.empty, Map.empty)
   8.103  
   8.104      val session_entries =
   8.105 -      (for ((name, res) <- results.iterator if res.parent_path.isDefined)
   8.106 -        yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
   8.107 -          { case (p, es) => (p, es.map(_._2).sorted) })
   8.108 -    for ((p, names) <- session_entries)
   8.109 -      Present.update_index(browser_info + Path.explode(p), names)
   8.110 +      (for ((name, res) <- results.iterator)
   8.111 +        yield (full_tree(name).chapter, name)).toList.groupBy(_._1).map(
   8.112 +          { case (chapter, es) => (chapter, es.map(_._2).sorted) })
   8.113 +    for ((chapter, names) <- session_entries)
   8.114 +      Present.update_chapter_index(browser_info, chapter, names)
   8.115  
   8.116      val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   8.117      if (rc != 0 && (verbose || !no_build)) {