# HG changeset patch # User wenzelm # Date 1363103244 -3600 # Node ID 6ac3c29a300e5d57effc59c5f14b7ca6ce8a4452 # Parent c3d02b3518c2afa9bedf00b2bf673bf7728b8ce6 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; diff -r c3d02b3518c2 -r 6ac3c29a300e NEWS --- a/NEWS Mon Mar 11 14:25:14 2013 +0100 +++ b/NEWS Tue Mar 12 16:47:24 2013 +0100 @@ -63,9 +63,9 @@ *** System *** -* Discontinued "isabelle usedir" option -P (remote path). Note that -usedir is legacy and superseded by "isabelle build" since -Isabelle2013. +* Discontinued "isabelle usedir" option -P (remote path) and -r (reset +session path). Note that usedir is legacy and superseded by "isabelle +build" since Isabelle2013. diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/System/session.ML --- a/src/Pure/System/session.ML Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/System/session.ML Tue Mar 12 16:47:24 2013 +0100 @@ -1,18 +1,16 @@ (* Title: Pure/System/session.ML Author: Markus Wenzel, TU Muenchen -Session management -- maintain state of logic images. +Session management -- internal state of logic images. *) signature SESSION = sig - val id: unit -> string list val name: unit -> string - val path: unit -> string list val welcome: unit -> string + val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> + string -> string * string -> bool * string -> bool -> unit val finish: unit -> unit - val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string -> string -> bool * string -> bool -> unit val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> string -> bool -> string list -> string -> string -> bool * string -> @@ -24,21 +22,10 @@ (* session state *) -val session = Unsynchronized.ref ([Context.PureN]: string list); +val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; val session_finished = Unsynchronized.ref false; -fun id () = ! session; -fun name () = "Isabelle/" ^ List.last (! session); - - -(* access path *) - -val session_path = Unsynchronized.ref ([]: string list); - -fun path () = ! session_path; - - -(* welcome *) +fun name () = "Isabelle/" ^ #name (! session); fun welcome () = if Distribution.is_official then @@ -46,22 +33,21 @@ else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; -(* add_path *) +(* init *) -fun add_path reset s = - let val sess = ! session @ [s] in - (case duplicates (op =) sess of - [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) - | dups => error ("Duplicate session identifiers " ^ commas_quote dups)) - end; - - -(* init_name *) - -fun init_name reset parent name = - if not (member (op =) (! session) parent) orelse not (! session_finished) then +fun init build info info_path doc doc_graph doc_output doc_variants + parent (chapter, name) doc_dump verbose = + if #name (! session) <> parent orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) - else (add_path reset name; session_finished := false); + else + let + val _ = session := {chapter = chapter, name = name}; + val _ = session_finished := false; + in + Present.init build info info_path (if doc = "false" then "" else doc) + doc_graph doc_output doc_variants (chapter, name) + doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) + end; (* finish *) @@ -77,7 +63,7 @@ session_finished := true); -(* use_dir *) +(* timing within ML *) fun with_timing name verbose f x = let @@ -99,21 +85,13 @@ else (); in y end; -fun init build reset info info_path doc doc_graph doc_output doc_variants - parent name doc_dump verbose = - (init_name reset parent name; - Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output - doc_variants (path ()) name doc_dump verbose - (map Thy_Info.get_theory (Thy_Info.get_names ()))); -local +(* use_dir *) fun read_variants strs = rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs))) |> filter_out (fn (_, s) => s = "-"); -in - fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent name doc_dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = @@ -123,13 +101,15 @@ Output.physical_stderr "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; val _ = + if not reset then () + else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n"; + val _ = if rpath = "" then () - else - Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n"; + else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n"; val _ = - init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name - doc_dump verbose; + init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants) + parent ("Unsorted", name) doc_dump verbose; val res1 = (use |> with_timing item timing |> Exn.capture) root; val res2 = Exn.capture finish (); in ignore (Par_Exn.release_all [res1, res2]) end) @@ -144,5 +124,3 @@ handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); end; - -end; diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Thy/html.ML Tue Mar 12 16:47:24 2013 +0100 @@ -22,12 +22,11 @@ val verbatim: string -> text val begin_document: string -> text val end_document: text - val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text + val begin_session_index: string -> (Url.T * string) list -> Url.T -> text val applet_pages: string -> Url.T * string -> (string * string) list val theory_entry: Url.T * string -> text - val session_entries: (Url.T * string) list -> text val theory_source: text -> text - val begin_theory: Url.T * string -> string -> (Url.T option * string) list -> + val begin_theory: string -> (Url.T option * string) list -> (Url.T * Url.T * bool) list -> text -> text val external_file: Url.T -> string -> text end; @@ -288,15 +287,11 @@ val end_document = "\n\n\n\n"; -fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); -val up_link = gen_link "Up"; -val back_link = gen_link "Back"; - (* session index *) -fun begin_index up (index_path, session) docs graph = - begin_document ("Index of " ^ session) ^ up_link up ^ +fun begin_session_index session docs graph = + begin_document ("Session " ^ plain session) ^ para ("View " ^ href_path graph "theory dependencies" ^ implode (map (fn (p, name) => "
\nView " ^ href_path p name) docs)) ^ "\n\n
\n

Theories

\n" - | session_entries es = - "\n
\n
\n\ - \

Sessions

\n"; +fun theory_entry (p, s) = "
  • " ^ href_path p (plain s) ^ "
    • \n"; (* theory *) @@ -350,9 +340,8 @@ fun file (href, path, loadit) = href_path href (if loadit then file_path path else enclose "(" ")" (file_path path)); - fun theory up A = - begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ - command "theory" ^ " " ^ name A; + fun theory A = + begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A; fun imports Bs = keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); @@ -360,8 +349,8 @@ fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "
    \n"; in -fun begin_theory up A Bs Ps body = - theory up A ^ "
    \n" ^ +fun begin_theory A Bs Ps body = + theory A ^ "
    \n" ^ imports Bs ^ "
    \n" ^ (if null Ps then "" else uses Ps) ^ body; diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Thy/html.scala Tue Mar 12 16:47:24 2013 +0100 @@ -11,7 +11,7 @@ object HTML { - // encode text + /* encode text */ def encode(text: String): String = { @@ -29,7 +29,27 @@ } - // common markup elements + /* document */ + + val end_document = "\n
    \n\n\n" + + def begin_document(title: String): String = + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "" + encode(title) + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "
    " + + "

    " + encode(title) + "

    \n" + + + /* common markup elements */ def session_entry(name: String): String = XML.string_of_tree( @@ -37,11 +57,11 @@ List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), List(XML.Text(name)))))) + "\n" - def session_entries(names: List[String]): String = - if (names.isEmpty) "" - else - "\n
    \n
    \n" + - "

    Sessions

    \n"; - - val end_document = "\n
    \n\n\n" + def chapter_index(chapter: String, sessions: List[String]): String = + { + begin_document("Isabelle/" + chapter + " sessions") + + (if (sessions.isEmpty) "" + else "
    ") + + end_document + } } diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Thy/present.ML Tue Mar 12 16:47:24 2013 +0100 @@ -14,8 +14,8 @@ include BASIC_PRESENT val session_name: theory -> string val read_variant: string -> string * string - val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string list -> string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) + val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> + string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit val theory_source: string -> (unit -> HTML.text) -> unit @@ -44,16 +44,6 @@ val graph_pdf_path = Path.basic "session_graph.pdf"; val graph_eps_path = Path.basic "session_graph.eps"; -val session_path = Path.basic ".session"; -val session_entries_path = Path.explode ".session/entries"; -val pre_index_path = Path.explode ".session/pre-index"; - -fun mk_rel_path [] ys = Path.make ys - | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent) - | mk_rel_path (ps as x :: xs) (qs as y :: ys) = - if x = y then mk_rel_path xs ys - else Path.appends (replicate (length ps) Path.parent @ [Path.make qs]); - fun show_path path = Path.implode (Path.append (File.pwd ()) path); @@ -62,34 +52,41 @@ structure Browser_Info = Theory_Data ( - type T = {name: string, session: string list}; - val empty = {name = "", session = []}: T; + type T = {chapter: string, name: string}; + val empty = {chapter = "Unsorted", name = "Unknown"}: T; (* FIXME !? *) fun extend _ = empty; fun merge _ = empty; ); -val put_info = Browser_Info.put; -val get_info = Browser_Info.get; -val session_name = #name o get_info; +val session_name = #name o Browser_Info.get; +val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get; (** graphs **) fun ID_of sess s = space_implode "/" (sess @ [s]); -fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy); +fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy); +fun theory_link curr_chapter thy = + let + val chapter = #chapter (Browser_Info.get thy); + val thy_html = html_path (Context.theory_name thy); + in + if curr_chapter = chapter then thy_html + else Path.appends [Path.parent, Path.basic chapter, thy_html] + end; (*retrieve graph data from initial collection of theories*) -fun init_graph curr_sess = rev o map (fn thy => +fun init_graph curr_chapter = rev o map (fn thy => let - val name = Context.theory_name thy; - val {name = sess_name, session} = get_info thy; + val {chapter, name = session_name} = Browser_Info.get thy; + val thy_name = Context.theory_name thy; val entry = - {name = name, ID = ID_of session name, dir = sess_name, - path = - if null session then "" - else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), + {name = thy_name, + ID = ID_of [chapter, session_name] thy_name, + dir = session_name, + path = Path.implode (theory_link curr_chapter thy), unfold = false, parents = map ID_of_thy (Theory.parents_of thy), content = []}; @@ -127,8 +124,8 @@ val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []); -fun init_browser_info curr_sess thys = make_browser_info - (Symtab.empty, [], [], [], init_graph curr_sess thys); +fun init_browser_info chapter thys = + make_browser_info (Symtab.empty, [], [], [], init_graph chapter thys); fun map_browser_info f {theories, files, tex_index, html_index, graph} = make_browser_info (f (theories, files, tex_index, html_index, graph)); @@ -186,16 +183,16 @@ (* session_info *) type session_info = - {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, + {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, documents: (string * string) list, doc_dump: (bool * string), verbose: bool, readme: Path.T option}; fun make_session_info - (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output, + (name, chapter, info_path, info, doc_format, doc_graph, doc_output, documents, doc_dump, verbose, readme) = - {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, - info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, + {name = name, chapter = chapter, info_path = info_path, info = info, + doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, documents = documents, doc_dump = doc_dump, verbose = verbose, readme = readme}: session_info; @@ -204,36 +201,12 @@ val session_info = Unsynchronized.ref (NONE: session_info option); -fun session_default x f = (case ! session_info of NONE => x | SOME info => f info); +fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); (** document preparation **) -(* maintain session index *) - -val session_entries = - HTML.session_entries o - map (fn name => (Url.File (Path.append (Path.basic name) index_path), name)); - -fun get_entries dir = - split_lines (File.read (Path.append dir session_entries_path)); - -fun put_entries entries dir = - File.write (Path.append dir session_entries_path) (cat_lines entries); - - -fun create_index dir = - File.read (Path.append dir pre_index_path) ^ - session_entries (get_entries dir) ^ HTML.end_document - |> File.write (Path.append dir index_path); - -fun update_index dir name = - (case try get_entries dir of - NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir) - | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); - - (* document variants *) fun read_variant str = @@ -245,19 +218,14 @@ (* init session *) -fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); - -fun init build info info_path doc doc_graph document_output doc_variants path name - (doc_dump as (_, dump_prefix)) verbose thys = +fun init build info info_path doc doc_graph document_output doc_variants + (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys = if not build andalso not info andalso doc = "" andalso dump_prefix = "" then (browser_info := empty_browser_info; session_info := NONE) else let - 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 (Path.explode info_path)) sess_prefix; - val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output); + val doc_output = + if document_output = "" then NONE else SOME (Path.explode document_output); val documents = if doc = "" then [] @@ -266,8 +234,6 @@ else (); []) else doc_variants; - val parent_index_path = Path.append Path.parent index_path; - val index_up_lnk = Url.File parent_index_path; val readme = if File.exists readme_html_path then SOME readme_html_path else if File.exists readme_path then SOME readme_path @@ -276,13 +242,13 @@ val docs = (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; - val index_text = HTML.begin_index (index_up_lnk, parent_name) - (Url.File index_path, session_name) docs (Url.explode "medium.html"); + val index_text = (* FIXME move to finish!? *) + HTML.begin_session_index name docs (Url.explode "medium.html"); in session_info := - SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc, + SOME (make_session_info (name, chapter, info_path, info, doc, doc_graph, doc_output, documents, doc_dump, verbose, readme)); - browser_info := init_browser_info path thys; + browser_info := init_browser_info chapter thys; add_html_index (0, index_text) end; @@ -331,15 +297,18 @@ fun finish () = - session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output, - documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} => + with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output, + documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; - val parent_html_prefix = Path.append html_prefix Path.parent; + + val chapter_prefix = Path.append info_path (Path.basic chapter); + val session_prefix = Path.append chapter_prefix (Path.basic name); fun finish_html (a, {html, ...}: theory_info) = - File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); + File.write_buffer (Path.append session_prefix (html_path a)) + (Buffer.add HTML.end_document html); val sorted_graph = sorted_index graph; val opt_graphs = @@ -349,21 +318,19 @@ val _ = if info then - (Isabelle_System.mkdirs (Path.append html_prefix session_path); - File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); - File.write (Path.append html_prefix session_entries_path) ""; - create_index html_prefix; - if length path > 1 then update_index parent_html_prefix name else (); - (case readme of NONE => () | SOME path => File.copy path html_prefix); - Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph; + (Isabelle_System.mkdirs session_prefix; + File.write_buffer (Path.append session_prefix index_path) + (index_buffer html_index |> Buffer.add HTML.end_document); + (case readme of NONE => () | SOME path => File.copy path session_prefix); + Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph; Isabelle_System.isabelle_tool "browser" "-b"; - File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; - List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) + File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; + List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/etc/isabelle.css") html_prefix; + File.copy (Path.explode "~~/etc/isabelle.css") session_prefix; List.app finish_html thys; List.app (uncurry File.write) files; - if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") + if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") else ()) else (); @@ -409,7 +376,7 @@ val jobs = (if info orelse is_none doc_output then - map (document_job html_prefix true) documents + map (document_job session_prefix true) documents else []) @ (case doc_output of NONE => [] @@ -424,30 +391,23 @@ (* theory elements *) -fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info); +fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info); fun theory_source name mk_text = - session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); + with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); fun theory_output name s = - session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s)); + with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s)); -fun parent_link curr_session thy = +fun begin_theory update_time dir thy = + with_session_info thy (fn {name = session_name, chapter, info_path, ...} => let - val {name = _, session} = get_info thy; - val name = Context.theory_name thy; - val link = - if null session then NONE - else SOME (Url.File (Path.append (mk_rel_path curr_session session) (html_path name))); - in (link, name) end; - -fun begin_theory update_time dir thy = - session_default thy (fn {name = sess_name, session, path, html_prefix, ...} => - let + val path = [chapter, session_name]; val name = Context.theory_name thy; val parents = Theory.parents_of thy; - val parent_specs = map (parent_link path) parents; + val parent_specs = parents |> map (fn parent => + (SOME (Url.File (theory_link chapter parent)), name)); val files = []; (* FIXME *) val files_html = files |> map (fn (raw_path, loadit) => @@ -455,18 +415,19 @@ val path = File.check_file (File.full_path dir raw_path); val base = Path.base path; val base_html = html_ext base; - val _ = add_file (Path.append html_prefix base_html, - HTML.external_file (Url.File base) (File.read path)); + (* FIXME retain file path!? *) + val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name]; + val _ = + add_file (Path.append session_prefix base_html, + HTML.external_file (Url.File base) (File.read path)); in (Url.File base_html, Url.File raw_path, loadit) end); fun prep_html_source (tex_source, html_source, html) = - let - val txt = HTML.begin_theory (Url.File index_path, session) - name parent_specs files_html (Buffer.content html_source) + let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source) in (tex_source, Buffer.empty, Buffer.add txt html) end; val entry = - {name = name, ID = ID_of path name, dir = sess_name, unfold = true, + {name = name, ID = ID_of path name, dir = session_name, unfold = true, path = Path.implode (html_path name), parents = map ID_of_thy parents, content = []}; @@ -475,7 +436,7 @@ add_graph_entry (update_time, entry); add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); add_tex_index (update_time, Latex.theory_entry name); - put_info {name = sess_name, session = path} thy + Browser_Info.put {chapter = chapter, name = session_name} thy end); diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Thy/present.scala Tue Mar 12 16:47:24 2013 +0100 @@ -9,33 +9,29 @@ object Present { - /* maintain session index -- NOT thread-safe */ + /* maintain chapter index -- NOT thread-safe */ private val index_path = Path.basic("index.html") - private val session_entries_path = Path.explode(".session/entries") - private val pre_index_path = Path.explode(".session/pre-index") + private val sessions_path = Path.basic(".sessions") - private def get_entries(dir: Path): List[String] = - split_lines(File.read(dir + session_entries_path)) + private def read_sessions(dir: Path): List[String] = + split_lines(File.read(dir + sessions_path)) - private def put_entries(entries: List[String], dir: Path): Unit = - File.write(dir + session_entries_path, cat_lines(entries)) + private def write_sessions(dir: Path, sessions: List[String]): Unit = + File.write(dir + sessions_path, cat_lines(sessions)) - def create_index(dir: Path): Unit = - File.write(dir + index_path, - File.read(dir + pre_index_path) + - HTML.session_entries(get_entries(dir)) + - HTML.end_document) + def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[String]): Unit = + { + val dir = info_path + Path.basic(chapter) + Isabelle_System.mkdirs(dir) - def update_index(dir: Path, names: List[String]): Unit = - try { - put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir) - create_index(dir) - } - catch { - case ERROR(msg) => - java.lang.System.err.println( - "### " + msg + "\n### Browser info: failed to update session index of " + dir) - } + val sessions0 = + try { split_lines(File.read(dir + sessions_path)) } + catch { case ERROR(_) => Nil } + + val sessions = sessions0.filterNot(new_sessions.contains) ::: new_sessions + write_sessions(dir, sessions) + File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) + } } diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Tools/build.ML Tue Mar 12 16:47:24 2013 +0100 @@ -109,11 +109,12 @@ fun build args_file = Command_Line.tool (fn () => let val (command_timings, (do_output, (options, (verbose, (browser_info, - (parent_name, (name, theories))))))) = + (parent_name, (chapter, (name, theories)))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in pair (list properties) (pair bool (pair Options.decode (pair bool (pair string - (pair string (pair string ((list (pair Options.decode (list string)))))))))) + (pair string (pair string (pair string + ((list (pair Options.decode (list string))))))))))) end; val document_variants = @@ -125,17 +126,14 @@ val _ = writeln ("\fSession.name = " ^ name); val _ = - (case Session.path () of - [] => () - | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path)); - val _ = - Session.init do_output false - (Options.bool options "browser_info") browser_info + Session.init do_output + (Options.bool options "browser_info") + (Path.explode browser_info) (Options.string options "document") (Options.bool options "document_graph") (Options.string options "document_output") document_variants - parent_name name + parent_name (chapter, name) (false, "") verbose; diff -r c3d02b3518c2 -r 6ac3c29a300e src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Mar 11 14:25:14 2013 +0100 +++ b/src/Pure/Tools/build.scala Tue Mar 12 16:47:24 2013 +0100 @@ -497,9 +497,10 @@ { import XML.Encode._ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, - pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))( + pair(string, pair(string, pair(string, + list(pair(Options.encode, list(Path.encode)))))))))))( (command_timings, (do_output, (info.options, (verbose, (browser_info, - (parent, (name, info.theories)))))))) + (parent, (info.chapter, (name, info.theories))))))))) })) private val env = @@ -595,7 +596,6 @@ private def log_gz(name: String): Path = log(name).ext("gz") private val SESSION_NAME = "\fSession.name = " - private val SESSION_PARENT_PATH = "\fSession.parent_path = " sealed case class Log_Info( @@ -754,7 +754,7 @@ } // scheduler loop - case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int) + case class Result(current: Boolean, heap: String, rc: Int) def sleep(): Unit = Thread.sleep(500) @@ -775,7 +775,7 @@ val res = job.join progress.echo(res.err) - val (parent_path, heap) = + val heap = if (res.rc == 0) { (output_dir + log(name)).file.delete @@ -784,13 +784,7 @@ File.write_gzip(output_dir + log_gz(name), sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out) - val parent_path = - if (job.info.options.bool("browser_info")) - res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)) - .map(_.substring(SESSION_PARENT_PATH.length)) - else None - - (parent_path, heap) + heap } else { (output_dir + Path.basic(name)).file.delete @@ -805,10 +799,10 @@ progress.echo("\n" + cat_lines(tail)) } - (None, no_heap) + no_heap } loop(pending - name, running - name, - results + (name -> Result(false, parent_path, heap, res.rc))) + results + (name -> Result(false, heap, res.rc))) //}}} case None if (running.size < (max_jobs max 1)) => //{{{ check/start next job @@ -816,7 +810,7 @@ case Some((name, info)) => val parent_result = info.parent match { - case None => Result(true, None, no_heap, 0) + case None => Result(true, no_heap, 0) case Some(parent) => results(parent) } val output = output_dir + Path.basic(name) @@ -839,10 +833,10 @@ val all_current = current && parent_result.current if (all_current) - loop(pending - name, running, results + (name -> Result(true, None, heap, 0))) + loop(pending - name, running, results + (name -> Result(true, heap, 0))) else if (no_build) { if (verbose) progress.echo("Skipping " + name + " ...") - loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, heap, 1))) } else if (parent_result.rc == 0 && !progress.stopped) { progress.echo((if (do_output) "Building " else "Running ") + name + " ...") @@ -853,7 +847,7 @@ } else { progress.echo(name + " CANCELLED") - loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, heap, 1))) } case None => sleep(); loop(pending, running, results) } @@ -874,11 +868,11 @@ else loop(queue, Map.empty, Map.empty) val session_entries = - (for ((name, res) <- results.iterator if res.parent_path.isDefined) - yield (res.parent_path.get, name)).toList.groupBy(_._1).map( - { case (p, es) => (p, es.map(_._2).sorted) }) - for ((p, names) <- session_entries) - Present.update_index(browser_info + Path.explode(p), names) + (for ((name, res) <- results.iterator) + yield (full_tree(name).chapter, name)).toList.groupBy(_._1).map( + { case (chapter, es) => (chapter, es.map(_._2).sorted) }) + for ((chapter, names) <- session_entries) + Present.update_chapter_index(browser_info, chapter, names) val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc }) if (rc != 0 && (verbose || !no_build)) {