--- a/src/HOL/ROOT Tue Nov 17 09:57:25 2020 +0000
+++ b/src/HOL/ROOT Tue Nov 17 09:57:37 2020 +0000
@@ -9,6 +9,8 @@
theories
Main (global)
Complex_Main (global)
+ document_theories
+ Tools.Code_Generator
document_files
"root.bib"
"root.tex"
--- a/src/HOL/document/root.tex Tue Nov 17 09:57:25 2020 +0000
+++ b/src/HOL/document/root.tex Tue Nov 17 09:57:37 2020 +0000
@@ -28,6 +28,7 @@
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
\parindent 0pt\parskip 0.5ex
+\input{Code_Generator.tex}
\input{session}
\pagestyle{headings}
--- a/src/Pure/ML/ml_console.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/ML/ml_console.scala Tue Nov 17 09:57:37 2020 +0000
@@ -72,7 +72,7 @@
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(
- options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
+ options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
POSIX_Interrupt.handler { process.interrupt } {
new TTY_Loop(process.stdin, process.stdout).join
--- a/src/Pure/ML/ml_process.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/ML/ml_process.scala Tue Nov 17 09:57:37 2020 +0000
@@ -85,6 +85,9 @@
session_base match {
case None => ""
case Some(base) =>
+ def print_symbols: List[(String, Int)] => String =
+ ML_Syntax.print_list(
+ ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_int))
def print_table: List[(String, String)] => String =
ML_Syntax.print_list(
ML_Syntax.print_pair(
@@ -100,7 +103,8 @@
ML_Syntax.print_list(ML_Syntax.print_string_bytes)))
"Resources.init_session" +
- "{session_positions = " + print_sessions(sessions_structure.session_positions) +
+ "{html_symbols = " + print_symbols(Symbol.codes) +
+ ", session_positions = " + print_sessions(sessions_structure.session_positions) +
", session_directories = " + print_table(sessions_structure.dest_session_directories) +
", session_chapters = " + print_table(sessions_structure.session_chapters) +
", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) +
@@ -197,11 +201,11 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
- val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+ val base_info = Sessions.base_info(options, logic, dirs = dirs).check
val store = Sessions.store(options)
-
val result =
- ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
+ ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
+ modes = modes, session_base = Some(base_info.base))
.result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))
--- a/src/Pure/PIDE/headless.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/PIDE/headless.scala Tue Nov 17 09:57:37 2020 +0000
@@ -558,7 +558,7 @@
val session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
extends isabelle.Resources(
- session_base_info.sessions_structure, session_base_info.check_base, log = log)
+ session_base_info.sessions_structure, session_base_info.check.base, log = log)
{
resources =>
--- a/src/Pure/PIDE/protocol.ML Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/PIDE/protocol.ML Tue Nov 17 09:57:37 2020 +0000
@@ -25,9 +25,10 @@
val _ =
Isabelle_Process.protocol_command "Prover.init_session"
- (fn [session_positions_yxml, session_directories_yxml, session_chapters_yxml,
+ (fn [html_symbols_yxml, session_positions_yxml, session_directories_yxml, session_chapters_yxml,
bibtex_entries_yxml, doc_names_yxml, global_theories_yxml, loaded_theories_yxml] =>
let
+ val decode_symbols = YXML.parse_body #> let open XML.Decode in list (pair string int) end;
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
val decode_sessions =
@@ -36,7 +37,8 @@
YXML.parse_body #> let open XML.Decode in list (pair string (list string)) end;
in
Resources.init_session
- {session_positions = decode_sessions session_positions_yxml,
+ {html_symbols = decode_symbols html_symbols_yxml,
+ session_positions = decode_sessions session_positions_yxml,
session_directories = decode_table session_directories_yxml,
session_chapters = decode_table session_chapters_yxml,
bibtex_entries = decode_bibtex_entries bibtex_entries_yxml,
--- a/src/Pure/PIDE/protocol.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/PIDE/protocol.scala Tue Nov 17 09:57:37 2020 +0000
@@ -289,6 +289,8 @@
{
import XML.Encode._
+ def encode_symbols(arg: List[(String, Int)]): String =
+ Symbol.encode_yxml(list(pair(string, int))(arg))
def encode_table(arg: List[(String, String)]): String =
Symbol.encode_yxml(list(pair(string, string))(arg))
def encode_list(arg: List[String]): String =
@@ -299,6 +301,7 @@
Symbol.encode_yxml(list(pair(string, list(string)))(arg))
protocol_command("Prover.init_session",
+ encode_symbols(Symbol.codes),
encode_sessions(resources.sessions_structure.session_positions),
encode_table(resources.sessions_structure.dest_session_directories),
encode_table(resources.sessions_structure.session_chapters),
--- a/src/Pure/PIDE/resources.ML Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/PIDE/resources.ML Tue Nov 17 09:57:37 2020 +0000
@@ -8,7 +8,8 @@
sig
val default_qualifier: string
val init_session:
- {session_positions: (string * Properties.T) list,
+ {html_symbols: (string * int) list,
+ session_positions: (string * Properties.T) list,
session_directories: (string * string) list,
session_chapters: (string * string) list,
bibtex_entries: (string * string list) list,
@@ -18,6 +19,7 @@
val finish_session_base: unit -> unit
val global_theory: string -> string option
val loaded_theory: string -> bool
+ val html_symbols: unit -> HTML.symbols
val check_session: Proof.context -> string * Position.T -> string
val session_chapter: string -> string
val check_doc: Proof.context -> string * Position.T -> string
@@ -56,7 +58,8 @@
{pos = Position.of_properties props, serial = serial ()};
val empty_session_base =
- {session_positions = []: (string * entry) list,
+ {html_symbols = HTML.no_symbols,
+ session_positions = []: (string * entry) list,
session_directories = Symtab.empty: Path.T list Symtab.table,
session_chapters = Symtab.empty: string Symtab.table,
bibtex_entries = Symtab.empty: string list Symtab.table,
@@ -68,11 +71,12 @@
Synchronized.var "Sessions.base" empty_session_base;
fun init_session
- {session_positions, session_directories, session_chapters,
+ {html_symbols, session_positions, session_directories, session_chapters,
bibtex_entries, docs, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
- {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+ {html_symbols = HTML.make_symbols html_symbols,
+ session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
session_directories =
fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
session_directories Symtab.empty,
@@ -85,7 +89,8 @@
fun finish_session_base () =
Synchronized.change global_session_base
(fn {global_theories, loaded_theories, ...} =>
- {session_positions = [],
+ {html_symbols = HTML.no_symbols,
+ session_positions = [],
session_directories = Symtab.empty,
session_chapters = Symtab.empty,
bibtex_entries = Symtab.empty,
@@ -98,6 +103,7 @@
fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
+fun html_symbols () = get_session_base #html_symbols;
fun check_name which kind markup ctxt arg =
Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg;
--- a/src/Pure/PIDE/session.ML Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/PIDE/session.ML Tue Nov 17 09:57:37 2020 +0000
@@ -9,7 +9,7 @@
val get_name: unit -> string
val welcome: unit -> string
val get_keywords: unit -> Keyword.keywords
- val init: HTML.symbols -> 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 symbols 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 symbols 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 Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/html.ML Tue Nov 17 09:57:37 2020 +0000
@@ -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 Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/html.scala Tue Nov 17 09:57:37 2020 +0000
@@ -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 Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/present.ML Tue Nov 17 09:57:37 2020 +0000
@@ -1,169 +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: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
- val finish: unit -> unit
- val begin_theory: int -> (unit -> 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 =
- {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
- verbose: bool, readme: Path.T option};
-
-fun make_session_info
- (symbols, name, chapter, info_path, info, verbose, readme) =
- {symbols = symbols, 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 symbols info info_path documents (chapter, name) verbose =
- let
- val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
-
- 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 (symbols, 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 mk_text thy =
- with_session_info thy (fn {symbols, 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 _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));
-
- 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 Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/present.scala Tue Nov 17 09:57:37 2020 +0000
@@ -1,14 +1,12 @@
/* Title: Pure/Thy/present.scala
Author: Makarius
-Theory presentation: HTML.
+Theory presentation: HTML and LaTeX documents.
*/
package isabelle
-import java.io.{File => JFile}
-
import scala.collection.immutable.SortedMap
@@ -74,27 +72,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 +236,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 +373,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 Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Tue Nov 17 09:57:37 2020 +0000
@@ -357,7 +357,7 @@
base: Base,
infos: List[Info])
{
- def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
+ def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
}
def base_info(options: Options,
@@ -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 =
@@ -812,7 +814,7 @@
})
def session_chapters: List[(String, String)] =
- build_topological_order.map(name => name -> apply(name).chapter)
+ imports_topological_order.map(name => name -> apply(name).chapter)
override def toString: String =
imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
--- a/src/Pure/Thy/thy_info.ML Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Thy/thy_info.ML Tue Nov 17 09:57:37 2020 +0000
@@ -18,11 +18,8 @@
val get_theory: string -> theory
val master_directory: string -> Path.T
val remove_thy: string -> unit
- type context =
- {options: Options.T,
- symbols: HTML.symbols,
- last_timing: Toplevel.transition -> Time.time}
- val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
+ type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time}
+ val use_theories: context -> string -> (string * Position.T) list -> unit
val use_thy: string -> unit
val script_thy: Position.T -> string -> theory -> theory
val register_thy: theory -> unit
@@ -56,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
@@ -65,11 +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)));
@@ -183,15 +182,10 @@
(* context *)
-type context =
- {options: Options.T,
- symbols: HTML.symbols,
- last_timing: Toplevel.transition -> Time.time};
+type context = {options: Options.T, last_timing: Toplevel.transition -> Time.time};
fun default_context (): context =
- {options = Options.default (),
- symbols = HTML.no_symbols,
- last_timing = K Time.zeroTime};
+ {options = Options.default (), last_timing = K Time.zeroTime};
(* scheduling loader tasks *)
@@ -300,7 +294,7 @@
fun eval_thy (context: context) update_time master_dir header text_pos text parents =
let
- val {options, symbols, last_timing} = context;
+ val {options, last_timing} = context;
val (name, _) = #name header;
val keywords =
fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
@@ -309,11 +303,7 @@
val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
val elements = Thy_Element.parse_elements keywords spans;
- fun init () =
- Resources.begin_theory master_dir header parents
- |> Present.begin_theory update_time
- (fn () => implode (map (HTML.present_span symbols keywords) spans));
-
+ 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);
@@ -438,13 +428,12 @@
(* use theories *)
-fun use_theories context qualifier master_dir imports =
- let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
+fun use_theories context qualifier imports =
+ let val (_, tasks) = require_thys context [] qualifier Path.current imports String_Graph.empty
in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
fun use_thy name =
- use_theories (default_context ()) Resources.default_qualifier
- Path.current [(name, Position.none)];
+ use_theories (default_context ()) Resources.default_qualifier [(name, Position.none)];
(* toplevel scripting -- without maintaining database *)
--- a/src/Pure/Tools/build.ML Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Tools/build.ML Tue Nov 17 09:57:37 2020 +0000
@@ -55,10 +55,9 @@
(* build theories *)
-fun build_theories symbols last_timing qualifier master_dir (options, thys) =
+fun build_theories last_timing qualifier (options, thys) =
let
- val context =
- {options = options, symbols = symbols, last_timing = last_timing};
+ val context = {options = options, last_timing = last_timing};
val condition = space_explode "," (Options.string options "condition");
val conds = filter_out (can getenv_strict) condition;
in
@@ -66,7 +65,7 @@
(Options.set_default options;
Isabelle_Process.init_options ();
Future.fork I;
- (Thy_Info.use_theories context qualifier master_dir
+ (Thy_Info.use_theories context qualifier
|>
(case Options.string options "profiling" of
"" => I
@@ -87,34 +86,30 @@
Isabelle_Process.protocol_command "build_session"
(fn [args_yxml] =>
let
- val (symbol_codes, (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, (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 (((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;
- val symbols = HTML.make_symbols symbol_codes;
-
fun build () =
let
val _ =
Resources.init_session
- {session_positions = session_positions,
+ {html_symbols = html_symbols,
+ session_positions = session_positions,
session_directories = session_directories,
session_chapters = session_chapters,
bibtex_entries = bibtex_entries,
@@ -122,21 +117,13 @@
global_theories = global_theories,
loaded_theories = loaded_theories};
- val _ =
- Session.init
- symbols
- (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);
val res1 =
theories |>
- (List.app (build_theories symbols last_timing session_name master_dir)
+ (List.app (build_theories last_timing session_name)
|> session_timing
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
--- a/src/Pure/Tools/build.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Tools/build.scala Tue Nov 17 09:57:37 2020 +0000
@@ -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,21 @@
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(Options.encode, list(pair(string, properties)))),
+ pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string,
+ pair(string, 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, (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 +370,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) }
--- a/src/Pure/Tools/server_commands.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Pure/Tools/server_commands.scala Tue Nov 17 09:57:37 2020 +0000
@@ -73,8 +73,7 @@
val base_info =
Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
- include_sessions = args.include_sessions)
- val base = base_info.check_base
+ include_sessions = args.include_sessions).check
val results =
Build.build(options,
--- a/src/Tools/VSCode/src/build_vscode.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Tools/VSCode/src/build_vscode.scala Tue Nov 17 09:57:37 2020 +0000
@@ -20,7 +20,7 @@
def build_grammar(options: Options, progress: Progress = new Progress)
{
val logic = Grammar.default_logic
- val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
+ val keywords = Sessions.base_info(options, logic).check.base.overall_syntax.keywords
val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
progress.echo(output_path.implode)
--- a/src/Tools/VSCode/src/grammar.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Tools/VSCode/src/grammar.scala Tue Nov 17 09:57:37 2020 +0000
@@ -158,7 +158,7 @@
if (more_args.nonEmpty) getopts.usage()
val keywords =
- Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
+ Sessions.base_info(Options.init(), logic, dirs = dirs).check.base.overall_syntax.keywords
val output_path = output getOrElse Path.explode(default_output(logic))
Output.writeln(output_path.implode)
--- a/src/Tools/VSCode/src/server.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Tools/VSCode/src/server.scala Tue Nov 17 09:57:37 2020 +0000
@@ -264,9 +264,7 @@
val base_info =
Sessions.base_info(
options, session_name, dirs = session_dirs, include_sessions = include_sessions,
- session_ancestor = session_ancestor, session_requirements = session_requirements)
-
- base_info.check_base
+ session_ancestor = session_ancestor, session_requirements = session_requirements).check
def build(no_build: Boolean = false): Build.Results =
Build.build(options,
--- a/src/Tools/VSCode/src/vscode_resources.scala Tue Nov 17 09:57:25 2020 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Nov 17 09:57:37 2020 +0000
@@ -73,7 +73,7 @@
val options: Options,
session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
- extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log)
+ extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log)
{
resources =>