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;
--- 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.
--- 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;
--- 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</div>\n</body>\n</html>\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) => "<br/>\nView " ^ href_path p name) docs)) ^
"\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
@@ -304,6 +299,8 @@
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
+fun back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name);
+
fun applet_pages session back =
let
val sizes =
@@ -329,14 +326,7 @@
in map applet_page sizes end;
-fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
-
-val theory_entry = entry;
-
-fun session_entries [] = "</ul>"
- | session_entries es =
- "</ul>\n</div>\n<div class=\"sessions\">\n\
- \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
+fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\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) ^ "<br/>\n";
in
-fun begin_theory up A Bs Ps body =
- theory up A ^ "<br/>\n" ^
+fun begin_theory A Bs Ps body =
+ theory A ^ "<br/>\n" ^
imports Bs ^ "<br/>\n" ^
(if null Ps then "" else uses Ps) ^
body;
--- 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</div>\n</body>\n</html>\n"
+
+ def begin_document(title: String): String =
+ "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
+ "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
+ "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
+ "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
+ "<head>\n" +
+ "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
+ "<title>" + encode(title) + "</title>\n" +
+ "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
+ "</head>\n" +
+ "\n" +
+ "<body>\n" +
+ "<div class=\"head\">" +
+ "<h1>" + encode(title) + "</h1>\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) "</ul>"
- else
- "</ul>\n</div>\n<div class=\"sessions\">\n" +
- "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
-
- val end_document = "\n</div>\n</body>\n</html>\n"
+ def chapter_index(chapter: String, sessions: List[String]): String =
+ {
+ begin_document("Isabelle/" + chapter + " sessions") +
+ (if (sessions.isEmpty) ""
+ else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
+ end_document
+ }
}
--- 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);
--- 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))
+ }
}
--- 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;
--- 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)) {