# HG changeset patch # User wenzelm # Date 1609858043 -3600 # Node ID 696819fe2424c2e50629370634de561664b48b36 # Parent 3e4df2e689ff516f1a0adba98957f69a129b0801 present theory using PIDE markup; diff -r 3e4df2e689ff -r 696819fe2424 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Tue Jan 05 14:21:18 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Tue Jan 05 15:47:23 2021 +0100 @@ -58,18 +58,20 @@ sealed case class Elements( html: Markup.Elements = Markup.Elements.empty, + entity: Markup.Elements = Markup.Elements.empty, language: Markup.Elements = Markup.Elements.empty) val elements1: Elements = Elements( html = Rendering.foreground_elements ++ Rendering.text_color_elements + - Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE) + Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE, + entity = Markup.Elements(Markup.THEORY)) val elements2: Elements = Elements( html = elements1.html ++ Rendering.markdown_elements, - language = elements1.language + Markup.Language.DOCUMENT) + language = Markup.Elements(Markup.Language.DOCUMENT)) /* HTML */ @@ -78,7 +80,10 @@ Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, HTML.descr.name) - def make_html(elements: Elements, xml: XML.Body): XML.Body = + def make_html( + elements: Elements, + entity_link: (Properties.T, XML.Body) => Option[XML.Tree], + xml: XML.Body): XML.Body = { def html_div(html: XML.Body): Boolean = html exists { @@ -93,6 +98,15 @@ def html_body(xml_body: XML.Body): XML.Body = xml_body flatMap { + case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) => + val body1 = html_body(body) + if (elements.entity(kind)) { + entity_link(props, body1) match { + case Some(link) => List(link) + case None => body1 + } + } + else body1 case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) => html_class(if (elements.language(name)) name else "", html_body(body)) case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => @@ -146,7 +160,7 @@ val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + Symbol.cartouche_decoded(name.path.file_name) - val body = make_html(elements, snapshot.xml_markup(elements = elements.html)) + val body = make_html(elements, (_, _) => None, snapshot.xml_markup(elements = elements.html)) html_context.html_document(title, body) } } @@ -376,31 +390,6 @@ HTML.link(info0.relative_path(info1) + html_name(name), body) } - def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = { - if (keywords.is_command(tok, Keyword.theory_end)) - List(Markup.KEYWORD2, Markup.KEYWORD) - else if (keywords.is_command(tok, Keyword.proof_asm)) - List(Markup.KEYWORD3, Markup.COMMAND) - else if (keywords.is_command(tok, Keyword.improper)) - List(Markup.KEYWORD1, Markup.IMPROPER, Markup.COMMAND) - else if (tok.is_command) List(Markup.KEYWORD1, Markup.COMMAND) - else if (tok.is_delimiter) List(Markup.DELIMITER, Markup.KEYWORD) - else if (tok.is_keyword) List(Markup.KEYWORD2, Markup.KEYWORD) - else if (tok.is_comment) List(Markup.COMMENT) - else { - tok.kind match { - case Token.Kind.VAR => List(Markup.VAR) - case Token.Kind.TYPE_IDENT => List(Markup.TFREE) - case Token.Kind.TYPE_VAR => List(Markup.TVAR) - case Token.Kind.STRING => List(Markup.STRING) - case Token.Kind.ALT_STRING => List(Markup.ALT_STRING) - case Token.Kind.VERBATIM => List(Markup.VERBATIM) - case Token.Kind.CARTOUCHE => List(Markup.CARTOUCHE) - case _ => Nil - } - } - } - def session_html( resources: Resources, session: String, @@ -456,6 +445,16 @@ val theories: List[XML.Body] = { var seen_files = List.empty[(Path, String, Document.Node.Name)] + + def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] = + (props, props, props) match { + case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) + if base.known_theories.isDefinedAt(theory) => + val node_name = base.known_theories(theory).name + Some(theory_link(deps, session, node_name, body)) + case _ => None + } + for { thy_name <- base.session_theories thy_command <- Build_Job.read_theory(db_context, resources, session, thy_name.theory) @@ -466,34 +465,6 @@ val snapshot = Document.State.init.snippet(thy_command) - val thy_body = - { - val syntax = base.theory_syntax(thy_name) - val keywords = syntax.keywords - val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path))) - - val imports_offset = base.known_theories(thy_name.theory).header.imports_offset - var token_offset = 1 - spans.flatMap(span => - { - val is_init = span.is_kind(keywords, Keyword.theory_begin, false) - span.content.flatMap(tok => - { - val text = HTML.text(tok.source) - val item = - if (is_init && imports_offset.isDefinedAt(token_offset)) { - List(theory_link(deps, session, imports_offset(token_offset), text)) - } - else text - - token_offset += tok.symbol_length - - (token_markups(keywords, tok) :\ item)( - { case (c, body) => List(HTML.span(c, body)) }) - }) - }) - } - val files = for { (src_path, xml) <- snapshot.xml_markup_blobs(elements = elements.html) @@ -518,12 +489,14 @@ 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), html_context.source(make_html(elements, xml)))) + List(html_context.head(file_title), + html_context.source(make_html(elements, entity_link, xml)))) List(HTML.link(file_name, HTML.text(file_title))) } val thy_title = "Theory " + thy_name.theory_base_name + val thy_body = make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html)) HTML.write_document(session_dir, html_name(thy_name), List(HTML.title(thy_title)), List(html_context.head(thy_title), html_context.source(thy_body)))