# HG changeset patch # User paulson # Date 1605607057 0 # Node ID 20f70d20e6f8c86057ed90077837daa57da18d6f # Parent 5e616a454b230f253043008347ca33b5868002d9# Parent 773ad766f1b898f0c1b3dfa76f1e33c38816b060 merged diff -r 773ad766f1b8 -r 20f70d20e6f8 src/HOL/ROOT --- 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" diff -r 773ad766f1b8 -r 20f70d20e6f8 src/HOL/document/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} diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/ML/ml_console.scala --- 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 diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/ML/ml_process.scala --- 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(_)) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/headless.scala --- 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 => diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/protocol.ML --- 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, diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/protocol.scala --- 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), diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/resources.ML --- 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; diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/PIDE/session.ML --- 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))); diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/html.ML --- 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

" ^ txt ^ "

\n"; - (* document *) @@ -142,27 +143,4 @@ val end_document = "\n\n\n\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) => "
\nView " ^ href_path p name) docs)) ^ - "\n\n
\n

Theories

\n
\n
\n
" "
\n" txt ^ - end_document; - end; diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/html.scala --- 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) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/present.ML --- 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 ^ "
\n" ^ + HTML.keyword symbols "imports" ^ " " ^ + space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^ + "
\n\n
\n
\n
" ::
+  body @ ["
\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; diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/present.scala --- 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) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/sessions.scala --- 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(", ", ", ")") diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Thy/thy_info.ML --- 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 *) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Tools/build.ML --- 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 (); diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Tools/build.scala --- 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) } diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Pure/Tools/server_commands.scala --- 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, diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Tools/VSCode/src/build_vscode.scala --- 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) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Tools/VSCode/src/grammar.scala --- 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) diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Tools/VSCode/src/server.scala --- 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, diff -r 773ad766f1b8 -r 20f70d20e6f8 src/Tools/VSCode/src/vscode_resources.scala --- 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 =>