--- a/Admin/components/components.sha1 Fri Nov 12 16:09:35 2021 +0100
+++ b/Admin/components/components.sha1 Fri Nov 12 17:22:06 2021 +0100
@@ -331,6 +331,7 @@
d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz
fb40145228f84513a9b083b54678a7d61b9c34c4 polyml-5.9-5d4caa8f7148.tar.gz
5f00a47b8f5180b33e68fcc6c343b061957a0a98 polyml-5.9-960de0cd0795.tar.gz
+7056b285af67902b32f5049349a064f073f05860 polyml-5.9-cc80e2b43c38.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
--- a/Admin/components/main Fri Nov 12 16:09:35 2021 +0100
+++ b/Admin/components/main Fri Nov 12 17:22:06 2021 +0100
@@ -17,7 +17,7 @@
minisat-2.2.1-1
nunchaku-0.5
opam-2.0.7
-polyml-5.9-5d4caa8f7148
+polyml-5.9-cc80e2b43c38
postgresql-42.2.24
scala-2.13.5
smbc-0.4.1
--- a/Admin/polyml/README Fri Nov 12 16:09:35 2021 +0100
+++ b/Admin/polyml/README Fri Nov 12 17:22:06 2021 +0100
@@ -3,7 +3,7 @@
This compilation of Poly/ML (https://www.polyml.org) is based on the
source distribution from
-https://github.com/polyml/polyml/commit/5d4caa8f7148 (shortly before
+https://github.com/polyml/polyml/commit/cc80e2b43c38 (shortly before
official version 5.9).
The Isabelle repository provides an administrative tool "isabelle
@@ -55,4 +55,4 @@
Makarius
- 07-Nov-2021
+ 12-Nov-2021
--- a/src/Pure/General/name_space.ML Fri Nov 12 16:09:35 2021 +0100
+++ b/src/Pure/General/name_space.ML Fri Nov 12 17:22:06 2021 +0100
@@ -115,7 +115,7 @@
fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
Position.make_entity_markup def serial kind (name, pos)
- ||> not (#def def) ? cons (Markup.def_theoryN, theory_long_name);
+ ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
--- a/src/Pure/Thy/presentation.scala Fri Nov 12 16:09:35 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Fri Nov 12 17:22:06 2021 +0100
@@ -20,11 +20,25 @@
sealed case class HTML_Document(title: String, content: String)
- def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
- new HTML_Context(cache)
+ abstract class HTML_Context
+ {
+ /* directory structure */
+
+ def root_dir: Path
+ def theory_session(name: Document.Node.Name): Sessions.Info
- final class HTML_Context private[Presentation](val cache: Term.Cache)
- {
+ def session_dir(info: Sessions.Info): Path =
+ root_dir + Path.explode(info.chapter_session)
+ def theory_path(name: Document.Node.Name): Path =
+ session_dir(theory_session(name)) + Path.explode(name.theory_base_name).html
+ def files_path(name: Document.Node.Name, path: Path): Path =
+ theory_path(name).dir + Path.explode("files") + path.squash.html
+
+
+ /* cached theory exports */
+
+ val cache: Term.Cache = Term.Cache.make()
+
private val already_presented = Synchronized(Set.empty[String])
def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
already_presented.change_result(presented =>
@@ -45,6 +59,9 @@
})
}
+
+ /* HTML content */
+
def head(title: String, rest: XML.Body = Nil): XML.Tree =
HTML.div("head", HTML.chapter(title) :: rest)
@@ -57,12 +74,14 @@
else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
}
+ val isabelle_css: String = File.read(HTML.isabelle_css)
+
def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document =
{
val content =
HTML.output_document(
List(
- HTML.style(fonts_css + "\n\n" + File.read(HTML.isabelle_css)),
+ HTML.style(fonts_css + "\n\n" + isabelle_css),
HTML.title(title)),
List(HTML.source(body)), css = "", structural = false)
HTML_Document(title, content)
@@ -96,6 +115,27 @@
object Entity_Context
{
+ object Theory_Ref
+ {
+ def unapply(props: Properties.T): Option[Document.Node.Name] =
+ (props, props, props) match {
+ case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
+ Some(Resources.file_node(Path.explode(thy_file), theory = theory))
+ case _ => None
+ }
+ }
+
+ object Entity_Ref
+ {
+ def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
+ (props, props, props, props) match {
+ case (Markup.Ref(_), Position.Def_File(def_file), Markup.Kind(kind), Markup.Name(name)) =>
+ val def_theory = Position.Def_Theory.unapply(props)
+ Some((Path.explode(def_file), def_theory, kind, name))
+ case _ => None
+ }
+ }
+
val empty: Entity_Context = new Entity_Context
def make(
@@ -149,19 +189,14 @@
override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
{
- (props, props, props, props, props) match {
- case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
- val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
+ props match {
+ case Theory_Ref(node_name) =>
node_relative(deps, session, node_name).map(html_dir =>
HTML.link(html_dir + html_name(node_name), body))
- case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
- Markup.Kind(kind), Markup.Name(name)) =>
- val file_path = Path.explode(def_file)
- val proper_thy_name =
- proper_string(def_theory) orElse
- (if (File.eq(node.path, file_path)) Some(node.theory) else None)
+ case Entity_Ref(file_path, def_theory, kind, name) =>
for {
- thy_name <- proper_thy_name
+ thy_name <-
+ def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
node_name = Resources.file_node(file_path, theory = thy_name)
html_dir <- node_relative(deps, session, node_name)
html_file = node_file(node_name)
@@ -415,13 +450,12 @@
val session_graph_path = Path.explode("session_graph.pdf")
val readme_path = Path.explode("README.html")
- val files_path = Path.explode("files")
def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
- def html_path(path: Path): String = (files_path + path.squash.html).implode
+ def files_path(src_path: Path): String = (Path.explode("files") + src_path.squash.html).implode
- private def node_file(node: Document.Node.Name): String =
- if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+ private def node_file(name: Document.Node.Name): String =
+ if (name.node.endsWith(".thy")) html_name(name) else files_path(name.path)
private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
{
@@ -460,20 +494,14 @@
progress: Progress = new Progress,
verbose: Boolean = false,
html_context: HTML_Context,
- session_elements: Elements,
- presentation: Context): Unit =
+ session_elements: Elements): Unit =
{
val hierarchy = deps.sessions_structure.hierarchy(session)
val info = deps.sessions_structure(session)
val options = info.options
val base = deps(session)
- def make_session_dir(name: String): Path =
- Isabelle_System.make_directory(
- presentation.dir(db_context.store, deps.sessions_structure(name)))
-
- val session_dir = make_session_dir(session)
- val presentation_dir = presentation.dir(db_context.store)
+ val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
Bytes.write(session_dir + session_graph_path,
graphview.Graph_File.make_pdf(options, base.session_graph_display))
@@ -538,10 +566,15 @@
val theories: List[XML.Body] =
{
sealed case class Seen_File(
- src_path: Path, file_name: String, thy_session: String, thy_name: Document.Node.Name)
+ src_path: Path, thy_name: Document.Node.Name, thy_session: String)
{
- def check(src_path1: Path, file_name1: String, thy_session1: String): Boolean =
- (src_path == src_path1 || file_name == file_name1) && thy_session == thy_session1
+ val files_path: Path = html_context.files_path(thy_name, src_path)
+
+ def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean =
+ {
+ val files_path1 = html_context.files_path(thy_name1, src_path1)
+ (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1
+ }
}
var seen_files = List.empty[Seen_File]
@@ -587,36 +620,34 @@
}
(for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
- val thy_session = base.theory_qualifier(thy.name)
- val thy_dir = make_session_dir(thy_session)
+ val thy_session = html_context.theory_session(thy.name)
+ val thy_dir = Isabelle_System.make_directory(html_context.session_dir(thy_session))
val files =
for { (src_path, file_html) <- thy.files_html }
yield {
- val file_name = html_path(src_path)
-
- seen_files.find(_.check(src_path, file_name, thy_session)) match {
- case None => seen_files ::= Seen_File(src_path, file_name, thy_session, thy.name)
+ seen_files.find(_.check(src_path, thy.name, thy_session.name)) match {
+ case None => seen_files ::= Seen_File(src_path, thy.name, thy_session.name)
case Some(seen_file) =>
- error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
+ error("Incoherent use of file name " + src_path + " as " + files_path(src_path) +
" in theory " + seen_file.thy_name + " vs. " + thy.name)
}
- val file_path = thy_dir + Path.explode(file_name)
+ val file_path = html_context.files_path(thy.name, src_path)
val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
HTML.write_document(file_path.dir, file_path.file_name,
List(HTML.title(file_title)), List(html_context.head(file_title), file_html),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
- List(HTML.link(file_name, HTML.text(file_title)))
+ List(HTML.link(files_path(src_path), HTML.text(file_title)))
}
val thy_title = "Theory " + thy.name.theory_base_name
HTML.write_document(thy_dir, html_name(thy.name),
List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
- if (thy_session == session) {
+ if (thy_session.name == session) {
Some(
List(HTML.link(html_name(thy.name),
HTML.text(thy.name.theory_base_name) :::
@@ -631,6 +662,6 @@
List(HTML.title(title + Isabelle_System.isabelle_heading())),
html_context.head(title, List(HTML.par(view_links))) ::
html_context.contents("Theories", theories),
- base = Some(presentation_dir))
+ base = Some(html_context.root_dir))
}
}
--- a/src/Pure/Tools/build.scala Fri Nov 12 16:09:35 2021 +0100
+++ b/src/Pure/Tools/build.scala Fri Nov 12 17:22:06 2021 +0100
@@ -506,16 +506,22 @@
Presentation.update_chapter(presentation_dir, chapter, entries)
}
- val html_context = Presentation.html_context(cache = store.cache)
-
using(store.open_database_context())(db_context =>
- for (info <- presentation_sessions) {
+ for (session <- presentation_sessions.map(_.name)) {
progress.expose_interrupt()
- progress.echo("Presenting " + info.name + " ...")
+ progress.echo("Presenting " + session + " ...")
+
+ val html_context =
+ new Presentation.HTML_Context {
+ override val cache: Term.Cache = store.cache
+ override def root_dir: Path = presentation_dir
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ deps.sessions_structure(deps(session).theory_qualifier(name))
+ }
Presentation.session_html(
- info.name, deps, db_context, progress = progress,
+ session, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
- Presentation.elements1, presentation = presentation)
+ Presentation.elements1)
})
}
}
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Nov 12 16:09:35 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Nov 12 17:22:06 2021 +0100
@@ -31,7 +31,12 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val html_context = Presentation.html_context()
+ val html_context =
+ new Presentation.HTML_Context {
+ override def root_dir: Path = Path.current
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ resources.sessions_structure(resources.session_base.theory_qualifier(name))
+ }
val document =
Presentation.html_document(snapshot, html_context, Presentation.elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
--- a/src/Tools/jEdit/src/document_model.scala Fri Nov 12 16:09:35 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Nov 12 17:22:06 2021 +0100
@@ -324,7 +324,13 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- val html_context = Presentation.html_context()
+ val html_context =
+ new Presentation.HTML_Context {
+ override def root_dir: Path = Path.current
+ override def theory_session(name: Document.Node.Name): Sessions.Info =
+ PIDE.resources.sessions_structure(
+ PIDE.resources.session_base.theory_qualifier(name))
+ }
val document =
Presentation.html_document(
snapshot, html_context, Presentation.elements2,