HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
--- a/src/Pure/PIDE/session.ML Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/PIDE/session.ML Mon Nov 16 22:23:04 2020 +0100
@@ -9,7 +9,7 @@
val get_name: unit -> string
val welcome: unit -> string
val get_keywords: unit -> Keyword.keywords
- val init: bool -> Path.T -> string list -> string -> string * string -> bool -> unit
+ val init: string -> string * string -> unit
val shutdown: unit -> unit
val finish: unit -> unit
end;
@@ -45,12 +45,11 @@
(* init *)
-fun init info info_path documents parent (chapter, name) verbose =
+fun init parent (chapter, name) =
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
if parent_name <> parent orelse not parent_finished then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
- else ({chapter = chapter, name = name}, false));
- Present.init info info_path documents (chapter, name) verbose);
+ else ({chapter = chapter, name = name}, false)));
(* finish *)
@@ -64,7 +63,6 @@
(shutdown ();
Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
Thy_Info.finish ();
- Present.finish ();
shutdown ();
update_keywords ();
Synchronized.change session (apsnd (K true)));
--- a/src/Pure/Thy/html.ML Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/html.ML Mon Nov 16 22:23:04 2020 +0100
@@ -1,5 +1,5 @@
(* Title: Pure/Thy/html.ML
- Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
+ Author: Makarius
HTML presentation elements.
*)
@@ -11,11 +11,14 @@
val no_symbols: symbols
val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
type text = string
+ val name: symbols -> string -> text
+ val keyword: symbols -> string -> text
+ val command: symbols -> string -> text
+ val href_name: string -> string -> string
+ val href_path: Url.T -> string -> string
+ val href_opt_path: Url.T option -> string -> string
val begin_document: symbols -> string -> text
val end_document: text
- val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text
- val theory_entry: symbols -> Url.T * string -> text
- val theory: symbols -> string -> (Url.T option * string) list -> text -> text
end;
structure HTML: HTML =
@@ -120,8 +123,6 @@
fun href_opt_path NONE txt = txt
| href_opt_path (SOME p) txt = href_path p txt;
-fun para txt = "\n<p>" ^ txt ^ "</p>\n";
-
(* document *)
@@ -142,27 +143,4 @@
val end_document = "\n</div>\n</body>\n</html>\n";
-
-(* session index *)
-
-fun begin_session_index symbols session graph docs =
- begin_document symbols ("Session " ^ output symbols 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";
-
-fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
-
-
-(* theory *)
-
-fun theory symbols A Bs txt =
- begin_document symbols ("Theory " ^ A) ^ "\n" ^
- command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
- keyword symbols "imports" ^ " " ^
- space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
- "<br/>\n" ^
- enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
- end_document;
-
end;
--- a/src/Pure/Thy/html.scala Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/html.scala Mon Nov 16 22:23:04 2020 +0100
@@ -155,6 +155,7 @@
def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
val no_text: XML.Tree = XML.Text("")
val break: XML.Body = List(XML.elem("br"))
+ val nl: XML.Body = List(XML.Text("\n"))
class Operator(val name: String)
{
@@ -197,9 +198,11 @@
def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
- def link(href: String, body: XML.Body = Nil): XML.Elem =
+ def link(href: String, body: XML.Body): XML.Elem =
XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
+ def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
+
def image(src: String, alt: String = ""): XML.Elem =
XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
--- a/src/Pure/Thy/present.ML Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/present.ML Mon Nov 16 22:23:04 2020 +0100
@@ -1,168 +1,75 @@
(* Title: Pure/Thy/present.ML
- Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
+ Author: Makarius
-Theory presentation: HTML and PDF-LaTeX documents.
+Theory presentation: HTML and LaTeX documents.
*)
signature PRESENT =
sig
- val init: bool -> Path.T -> string list -> string * string -> bool -> unit
- val finish: unit -> unit
- val begin_theory: int -> HTML.text -> theory -> theory
+ val document_html_name: theory -> Path.binding
+ val document_tex_name: theory -> Path.binding
+ val html_name: theory -> Path.T
+ val export_html: theory -> Command_Span.span list -> unit
end;
structure Present: PRESENT =
struct
-
-(** paths **)
-
-val html_ext = Path.ext "html";
-val html_path = html_ext o Path.basic;
-val index_path = Path.basic "index.html";
-val readme_html_path = Path.basic "README.html";
-val session_graph_path = Path.basic "session_graph.pdf";
-val document_path = Path.ext "pdf" o Path.basic;
-
-fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
-
+(** artefact names **)
-
-(** global browser info state **)
-
-(* type browser_info *)
-
-type browser_info =
- {html_theories: string Symtab.table,
- html_index: (int * string) list};
-
-fun make_browser_info (html_theories, html_index) : browser_info =
- {html_theories = html_theories, html_index = html_index};
-
-val empty_browser_info = make_browser_info (Symtab.empty, []);
+fun document_name ext thy =
+ Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
-fun map_browser_info f {html_theories, html_index} =
- make_browser_info (f (html_theories, html_index));
-
-
-(* state *)
-
-val browser_info = Synchronized.var "browser_info" empty_browser_info;
-fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);
-
-fun update_html name html = change_browser_info (apfst (Symtab.update (name, html)));
-
-fun add_html_index txt = change_browser_info (apsnd (cons txt));
+val document_html_name = document_name "html";
+val document_tex_name = document_name "tex";
-
-
-(** global session state **)
-
-(* session_info *)
-
-type session_info =
- {name: string, chapter: string, info_path: Path.T, info: bool,
- verbose: bool, readme: Path.T option};
-
-fun make_session_info (name, chapter, info_path, info, verbose, readme) =
- {name = name, chapter = chapter, info_path = info_path, info = info,
- verbose = verbose, readme = readme}: session_info;
+fun html_name thy = Path.basic (Context.theory_name thy ^ ".html");
-(* state *)
-
-val session_info = Unsynchronized.ref (NONE: session_info option);
-
-fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
-
-val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;
-
-fun is_session_theory thy =
- (case ! session_info of
- NONE => false
- | SOME {name, ...} => name = theory_qualifier thy);
-
-
-(** document preparation **)
-
-(* init session *)
-
-fun init info info_path documents (chapter, name) verbose =
- let
- val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
- val symbols = Resources.html_symbols ();
- val docs =
- (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
- map (fn name => (Url.File (document_path name), name)) documents;
- in
- session_info := SOME (make_session_info (name, chapter, info_path, info, verbose, readme));
- Synchronized.change browser_info (K empty_browser_info);
- add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
- end;
-
+(* theory as HTML *)
-(* finish session -- output all generated text *)
-
-fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
-fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
-
-fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} =>
- let
- val {html_theories, html_index} = Synchronized.value browser_info;
-
- val session_prefix = info_path + Path.basic chapter + Path.basic name;
-
- fun finish_html (a, html) = File.write (session_prefix + html_path a) html;
+local
- val _ =
- if info then
- (Isabelle_System.make_directory session_prefix;
- File.write_buffer (session_prefix + index_path)
- (index_buffer html_index |> Buffer.add HTML.end_document);
- (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
- Symtab.fold (K o finish_html) html_theories ();
- if verbose
- then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
- else ())
- else ();
- in
- Synchronized.change browser_info (K empty_browser_info);
- session_info := NONE
- end);
-
-
-(* theory elements *)
-
-fun theory_link (curr_chapter, curr_session) thy =
+fun get_session_chapter thy =
let
val session = Resources.theory_qualifier (Context.theory_long_name thy);
val chapter = Resources.session_chapter session;
- val link = html_path (Context.theory_name thy);
+ in (session, chapter) end;
+
+fun theory_link thy thy' =
+ let
+ val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
+ val link = html_name thy';
in
- if curr_session = session then SOME link
- else if curr_chapter = chapter then
- SOME (Path.parent + Path.basic session + link)
+ if session = session' then SOME link
+ else if chapter = chapter' then SOME (Path.parent + Path.basic session + link)
else if chapter = Context.PureN then NONE
else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
end;
-fun begin_theory update_time html thy =
- with_session_info thy (fn {name = session_name, chapter, ...} =>
- let
- val name = Context.theory_name thy;
+fun theory_document symbols A Bs body =
+ HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
+ HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^
+ HTML.keyword symbols "imports" ^ " " ^
+ space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^
+ "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
+ body @ ["</pre>\n", HTML.end_document];
+
+in
- val parent_specs =
- Theory.parents_of thy |> map (fn parent =>
- (Option.map Url.File (theory_link (chapter, session_name) parent),
- (Context.theory_name parent)));
+fun export_html thy spans =
+ let
+ val name = Context.theory_name thy;
+ val parents =
+ Theory.parents_of thy |> map (fn thy' =>
+ (Option.map Url.File (theory_link thy thy'), Context.theory_name thy'));
- val symbols = Resources.html_symbols ();
- val _ = update_html name (HTML.theory symbols name parent_specs html);
-
- val _ =
- if is_session_theory thy then
- add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name))
- else ();
- in thy end);
+ val symbols = Resources.html_symbols ();
+ val keywords = Thy_Header.get_keywords thy;
+ val body = map (HTML.present_span symbols keywords) spans;
+ val html = XML.blob (theory_document symbols name parents body);
+ in Export.export thy (document_html_name thy) html end
end;
+
+end;
--- a/src/Pure/Thy/present.scala Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/present.scala Mon Nov 16 22:23:04 2020 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/present.scala
Author: Makarius
-Theory presentation: HTML.
+Theory presentation: HTML and LaTeX documents.
*/
package isabelle
@@ -74,27 +74,72 @@
}
- /* finish session */
+ /* present session */
+
+ val session_graph_path = Path.explode("session_graph.pdf")
+ val readme_path = Path.basic("README.html")
+
+ def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
+ def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
+
+ def theory_link(name: Document.Node.Name): XML.Tree =
+ HTML.link(html_name(name), HTML.text(name.theory_base_name))
- def finish(
- browser_info: Path,
- graph_pdf: Bytes,
- info: Sessions.Info,
- name: String)
+ def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path =
{
- val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
- val session_fonts = session_prefix + Path.explode("fonts")
+ val info = deps.sessions_structure(session)
+ val options = info.options
+ val base = deps(session)
+
+ val session_dir = store.browser_info + info.chapter_session
+ val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
+ for (entry <- Isabelle_Fonts.fonts(hidden = true))
+ File.copy(entry.path, session_fonts)
+
+ Bytes.write(session_dir + session_graph_path,
+ graphview.Graph_File.make_pdf(options, base.session_graph_display))
+
+ val links =
+ {
+ val deps_link =
+ HTML.link(session_graph_path, HTML.text("theory dependencies"))
- if (info.options.bool("browser_info")) {
- Isabelle_System.make_directory(session_fonts)
+ val readme_links =
+ if ((info.dir + readme_path).is_file) {
+ File.copy(info.dir + readme_path, session_dir + readme_path)
+ List(HTML.link(readme_path, HTML.text("README")))
+ }
+ else Nil
- Bytes.write(session_prefix + session_graph_path, graph_pdf)
+ val document_links =
+ for ((name, _) <- info.documents)
+ yield HTML.link(Path.basic(name).pdf, HTML.text(name))
+
+ Library.separate(HTML.break ::: HTML.nl,
+ (deps_link :: readme_links ::: document_links).
+ map(link => HTML.text("View ") ::: List(link))).flatten
+ }
- HTML.write_isabelle_css(session_prefix)
+ val theories =
+ using(store.open_database(session))(db =>
+ for {
+ name <- base.session_theories
+ entry <- Export.read_entry(db, session, name.theory, document_html_name(name))
+ } yield name -> entry.uncompressed(cache = store.xz_cache))
+
+ val theories_body =
+ HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name)))
- for (entry <- Isabelle_Fonts.fonts(hidden = true))
- File.copy(entry.path, session_fonts)
- }
+ val title = "Session " + session
+ HTML.write_document(session_dir, "index.html",
+ List(HTML.title(title + " (" + Distribution.version + ")")),
+ HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
+ (if (theories.isEmpty) Nil
+ else List(HTML.div("theories", List(HTML.section("Theories"), theories_body)))))
+
+ for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html)
+
+ session_dir
}
@@ -193,7 +238,6 @@
/** build documents **/
val session_tex_path = Path.explode("session.tex")
- val session_graph_path = Path.explode("session_graph.pdf")
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
@@ -331,7 +375,7 @@
}
if (info.options.bool("browser_info") || doc_output.isEmpty) {
- output(store.browser_info + Path.basic(info.chapter) + Path.basic(session))
+ output(store.browser_info + info.chapter_session)
}
doc_output.foreach(output)
--- a/src/Pure/Thy/sessions.scala Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Nov 16 22:23:04 2020 +0100
@@ -459,6 +459,8 @@
export_files: List[(Path, Int, List[String])],
meta_digest: SHA1.Digest)
{
+ def chapter_session: Path = Path.basic(chapter) + Path.basic(name)
+
def deps: List[String] = parent.toList ::: imports
def deps_base(session_bases: String => Base): Base =
--- a/src/Pure/Thy/thy_info.ML Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Nov 16 22:23:04 2020 +0100
@@ -53,6 +53,7 @@
val _ =
Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+ (Present.export_html thy (map #span segments);
if exists (Toplevel.is_skipped_proof o #state) segments then ()
else
let
@@ -62,12 +63,12 @@
else
let
val thy_name = Context.theory_name thy;
- val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex");
+ val document_tex_name = Present.document_tex_name thy;
val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
in Export.export thy document_tex_name (XML.blob output) end
- end));
+ end)));
@@ -302,13 +303,7 @@
val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
val elements = Thy_Element.parse_elements keywords spans;
- val symbols = Resources.html_symbols ();
- val html = implode (map (HTML.present_span symbols keywords) spans);
-
- fun init () =
- Resources.begin_theory master_dir header parents
- |> Present.begin_theory update_time html;
-
+ fun init () = Resources.begin_theory master_dir header parents;
val (results, thy) =
cond_timeit true ("theory " ^ quote name)
(fn () => excursion keywords master_dir last_timing init elements);
--- a/src/Pure/Tools/build.ML Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Tools/build.ML Mon Nov 16 22:23:04 2020 +0100
@@ -86,25 +86,23 @@
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
- val (html_symbols, (command_timings, (verbose, (browser_info,
- (documents, (parent_name, (chapter, (session_name, (master_dir,
- (theories, (session_positions, (session_directories, (session_chapters,
- (doc_names, (global_theories, (loaded_theories, bibtex_entries)))))))))))))))) =
+ val (html_symbols, (command_timings, (parent_name, (chapter,
+ (session_name, (master_dir, (theories, (session_positions, (session_directories,
+ (session_chapters, (doc_names,
+ (global_theories, (loaded_theories, bibtex_entries))))))))))))) =
YXML.parse_body args_yxml |>
let
open XML.Decode;
val position = Position.of_properties o properties;
val path = Path.explode o string;
in
- pair (list (pair string int)) (pair (list properties) (pair bool (pair path
- (pair (list string) (pair string (pair string (pair string
- (pair path
- (pair (((list (pair Options.decode (list (pair string position))))))
- (pair (list (pair string properties))
- (pair (list (pair string string))
- (pair (list (pair string string)) (pair (list string)
- (pair (list (pair string string)) (pair (list string)
- (list (pair string (list string))))))))))))))))))
+ pair (list (pair string int)) (pair (list properties) (pair string (pair string
+ (pair string (pair path
+ (pair (((list (pair Options.decode (list (pair string position))))))
+ (pair (list (pair string properties)) (pair (list (pair string string))
+ (pair (list (pair string string)) (pair (list string)
+ (pair (list (pair string string)) (pair (list string)
+ (list (pair string (list string)))))))))))))))
end;
fun build () =
@@ -120,14 +118,7 @@
global_theories = global_theories,
loaded_theories = loaded_theories};
- val _ =
- Session.init
- (Options.default_bool "browser_info")
- browser_info
- documents
- parent_name
- (chapter, session_name)
- verbose;
+ val _ = Session.init parent_name (chapter, session_name);
val last_timing = get_timings (fold update_timings command_timings empty_timings);
--- a/src/Pure/Tools/build.scala Mon Nov 16 22:21:40 2020 +0100
+++ b/src/Pure/Tools/build.scala Mon Nov 16 22:23:04 2020 +0100
@@ -165,7 +165,6 @@
val options: Options = NUMA.policy_options(info.options, numa_node)
private val sessions_structure = deps.sessions_structure
- private val documents = info.documents.map(_._1)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
@@ -175,23 +174,22 @@
YXML.string_of_body(
{
import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode,
- pair(list(string), pair(string, pair(string, pair(string, pair(Path.encode,
+ pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
+ pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
pair(list(pair(string, properties)),
pair(list(pair(string, string)),
pair(list(pair(string, string)),
pair(list(string),
pair(list(pair(string, string)),
- pair(list(string), list(pair(string, list(string)))))))))))))))))))(
- (Symbol.codes, (command_timings0, (verbose, (store.browser_info,
- (documents, (parent, (info.chapter, (session_name, (Path.current,
- (info.theories,
+ pair(list(string), list(pair(string, list(string))))))))))))))))(
+ (Symbol.codes, (command_timings0, (parent, (info.chapter,
+ (session_name, (Path.current, (info.theories,
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.session_chapters,
(base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))))))
+ (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))
})
val env =
@@ -373,20 +371,23 @@
val document_errors =
try {
- if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && documents.nonEmpty) {
- val document_progress =
- new Progress {
- override def echo(msg: String): Unit =
- document_output.synchronized { document_output += msg }
- override def echo_document(path: Path): Unit =
- progress.echo_document(path)
- }
- Present.build_documents(session_name, deps, store, verbose = verbose,
- verbose_latex = true, progress = document_progress)
+ if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) {
+ if (info.documents.nonEmpty) {
+ val document_progress =
+ new Progress {
+ override def echo(msg: String): Unit =
+ document_output.synchronized { document_output += msg }
+ override def echo_document(path: Path): Unit =
+ progress.echo_document(path)
+ }
+ Present.build_documents(session_name, deps, store, verbose = verbose,
+ verbose_latex = true, progress = document_progress)
+ }
+ if (info.options.bool("browser_info")) {
+ val dir = Present.session_html(session_name, deps, store)
+ if (verbose) progress.echo("Browser info at " + dir.absolute)
+ }
}
- val graph_pdf =
- graphview.Graph_File.make_pdf(options, deps(session_name).session_graph_display)
- Present.finish(store.browser_info, graph_pdf, info, session_name)
Nil
}
catch { case Exn.Interrupt.ERROR(msg) => List(msg) }