# HG changeset patch # User wenzelm # Date 1605912454 -3600 # Node ID 5e7916535860f9b9b6b4c05a179aa3f7043ebe4b # Parent b1388cfb64bb65d4078aa4a04998ad2eec5e0577 generate theory HTML in Isabelle/Scala; discontinued HTML support in Isabelle/ML; diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Isar/keyword.scala Fri Nov 20 23:47:34 2020 +0100 @@ -88,6 +88,9 @@ PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) + val proof_asm = Set(PRF_ASM, PRF_ASM_GOAL) + val improper = Set(QED_SCRIPT, PRF_SCRIPT, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) + val theory_goal = Set(THY_GOAL, THY_GOAL_DEFN, THY_GOAL_STMT) val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL) val qed = Set(QED, QED_SCRIPT, QED_BLOCK) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Isar/token.scala Fri Nov 20 23:47:34 2020 +0100 @@ -328,6 +328,8 @@ def is_end: Boolean = is_command("end") def is_begin_or_command: Boolean = is_begin || is_command + def symbol_length: Symbol.Offset = Symbol.iterator(source).length + def content: String = if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source) else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/document.scala Fri Nov 20 23:47:34 2020 +0100 @@ -86,6 +86,9 @@ abbrevs: Thy_Header.Abbrevs = Nil, errors: List[String] = Nil) { + def imports_offset: Map[Int, Name] = + (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap + def imports: List[Name] = imports_pos.map(_._1) def append_errors(msgs: List[String]): Header = diff -r b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/resources.ML Fri Nov 20 23:47:34 2020 +0100 @@ -8,8 +8,7 @@ sig val default_qualifier: string val init_session: - {html_symbols: (string * int) list, - session_positions: (string * Properties.T) list, + {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, @@ -22,7 +21,6 @@ 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 last_timing: Toplevel.transition -> Time.time @@ -97,8 +95,7 @@ {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = - {html_symbols = HTML.no_symbols, - session_positions = []: (string * entry) list, + {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, @@ -111,12 +108,11 @@ Synchronized.var "Sessions.base" empty_session_base; fun init_session - {html_symbols, session_positions, session_directories, session_chapters, + {session_positions, session_directories, session_chapters, bibtex_entries, command_timings, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => - {html_symbols = HTML.make_symbols html_symbols, - session_positions = sort_by #1 (map (apsnd make_entry) session_positions), + {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, @@ -129,20 +125,18 @@ fun init_session_yxml yxml = let - val (html_symbols, (session_positions, (session_directories, (session_chapters, - (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories)))))))) = + val (session_positions, (session_directories, (session_chapters, + (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in - pair (list (pair string int)) - (pair (list (pair string properties)) - (pair (list (pair string string)) (pair (list (pair string string)) - (pair (list (pair string (list string))) (pair (list properties) - (pair (list string) (pair (list (pair string string)) (list string)))))))) + (pair (list (pair string properties)) + (pair (list (pair string string)) (pair (list (pair string string)) + (pair (list (pair string (list string))) (pair (list properties) + (pair (list string) (pair (list (pair string string)) (list string)))))))) end; in init_session - {html_symbols = html_symbols, - session_positions = session_positions, + {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, @@ -158,8 +152,7 @@ fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => - {html_symbols = HTML.no_symbols, - session_positions = [], + {session_positions = [], session_directories = Symtab.empty, session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, @@ -173,8 +166,6 @@ 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 b1388cfb64bb -r 5e7916535860 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Fri Nov 20 23:47:34 2020 +0100 @@ -28,15 +28,13 @@ import XML.Encode._ YXML.string_of_body( - pair(list(pair(string, int)), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), pair(list(string), - pair(list(pair(string, string)), list(string)))))))))( - (Symbol.codes, + pair(list(pair(string, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, @@ -44,7 +42,7 @@ (command_timings, (session_base.doc_names, (session_base.global_theories.toList, - session_base.loaded_theories.keys)))))))))) + session_base.loaded_theories.keys))))))))) } diff -r b1388cfb64bb -r 5e7916535860 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/ROOT.ML Fri Nov 20 23:47:34 2020 +0100 @@ -232,7 +232,6 @@ ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; -ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Nov 20 14:29:21 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: Pure/Thy/html.ML - Author: Makarius - -HTML presentation elements. -*) - -signature HTML = -sig - type symbols - val make_symbols: (string * int) list -> symbols - 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 begin_document: symbols -> string -> text - val end_document: text -end; - -structure HTML: HTML = -struct - - -(* common markup *) - -fun span "" = ("", "") - | span class = ("", ""); - -val enclose_span = uncurry enclose o span; - -val hidden = enclose_span Markup.hiddenN; - - -(* symbol output *) - -abstype symbols = Symbols of string Symtab.table -with - -fun make_symbols codes = - let - val mapping = - map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @ - [("'", "'"), - ("\<^bsub>", hidden "⇘" ^ ""), - ("\<^esub>", hidden "⇙" ^ ""), - ("\<^bsup>", hidden "⇗" ^ ""), - ("\<^esup>", hidden "⇖" ^ "")]; - in Symbols (fold Symtab.update mapping Symtab.empty) end; - -val no_symbols = make_symbols []; - -fun output_sym (Symbols tab) s = - (case Symtab.lookup tab s of - SOME x => x - | NONE => XML.text s); - -end; - -local - -fun output_markup (bg, en) symbols s1 s2 = - hidden s1 ^ enclose bg en (output_sym symbols s2); - -val output_sub = output_markup ("", ""); -val output_sup = output_markup ("", ""); -val output_bold = output_markup (span "bold"); - -fun output_syms _ [] result = implode (rev result) - | output_syms symbols (s1 :: rest) result = - let - val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)); - val (s, r) = - if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss) - else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss) - else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss) - else (output_sym symbols s1, rest); - in output_syms symbols r (s :: result) end; - -in - -fun output symbols str = output_syms symbols (Symbol.explode str) []; - -end; - - -(* presentation *) - -fun present_span symbols keywords = - let - fun present_markup (name, props) = - (case Properties.get props Markup.kindN of - SOME kind => - if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I - | NONE => I) #> enclose_span name; - fun present_token tok = - fold_rev present_markup (Token.markups keywords tok) - (output symbols (Token.unparse tok)); - in implode o map present_token o Command_Span.content end; - - - -(** HTML markup **) - -type text = string; - - -(* atoms *) - -val name = enclose "" "" oo output; -val keyword = enclose "" "" oo output; -val command = enclose "" "" oo output; - - -(* misc *) - -fun href_name s txt = "" ^ txt ^ ""; -fun href_path path txt = href_name (Url.implode path) txt; - - -(* document *) - -fun begin_document symbols title = - XML.header ^ - "\n" ^ - "\n" ^ - "\n" ^ - "\n" ^ - "" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "\n" ^ - "\n" ^ - "\n" ^ - "\n" ^ - "\n" ^ - "
" ^ - "

" ^ output symbols title ^ "

\n"; - -val end_document = "\n
\n\n\n"; - -end; diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Thy/presentation.scala Fri Nov 20 23:47:34 2020 +0100 @@ -206,8 +206,30 @@ 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 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( session: String, @@ -248,24 +270,62 @@ map(link => HTML.text("View ") ::: List(link))).flatten } + def theory_link(name1: Document.Node.Name, body: XML.Body): XML.Tree = + { + val session1 = base.theory_qualifier(name1) + val info1 = deps.sessions_structure(session1) + val prefix = + if (session == session1) "" + else if (info.chapter == info1.chapter) "../" + session1 + "/" + else "../../" + info1.chapter + "/" + session1 + "/" + HTML.link(prefix + html_name(name1), body) + } + val theories = - using(Export.open_database_context(deps.sessions_structure, store))(context => - for { - name <- base.session_theories - entry <- context.try_entry(session, name.theory, document_html_name(name)) - } yield name -> entry.uncompressed(cache = store.xz_cache)) + for (name <- base.session_theories) + yield { + val syntax = base.theory_syntax(name) + val keywords = syntax.keywords + val spans = syntax.parse_spans(Symbol.decode(File.read(name.path))) - val theories_body = - HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name))) + val thy_body = + { + val imports_offset = base.known_theories(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(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 title = "Theory " + name.theory_base_name + HTML.write_document(session_dir, html_name(name), + List(HTML.title(title)), + HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body))) + + List(HTML.link(html_name(name), HTML.text(name.theory_base_name))) + } 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) + else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories)))))) session_dir } diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Nov 20 23:47:34 2020 +0100 @@ -80,6 +80,9 @@ def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = loaded_theory_syntax(name.theory) + def theory_syntax(name: Document.Node.Name): Outer_Syntax = + loaded_theory_syntax(name) getOrElse overall_syntax + def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax } diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Nov 20 14:29:21 2020 +0100 +++ b/src/Pure/Thy/thy_info.ML Fri Nov 20 23:47:34 2020 +0100 @@ -35,59 +35,8 @@ fun document_name ext thy = Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); -val document_html_name = document_name "html"; val document_tex_name = document_name "tex"; -fun html_name thy = Path.basic (Context.theory_name thy ^ ".html"); - - -(* theory as HTML *) - -local - -fun get_session_chapter thy = - let - val session = Resources.theory_qualifier (Context.theory_long_name thy); - val chapter = Resources.session_chapter session; - 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 session = session' then link - else if chapter = chapter' then Path.parent + Path.basic session' + link - else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link - end; - -fun theory_document symbols A Bs body = - HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^ - HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "
\n" ^ - (if null Bs then "" - else - HTML.keyword symbols "imports" ^ " " ^ - space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "
\n") ^ - "\n\n
\n
" ::
-  body @ ["
\n", HTML.end_document]; - -in - -fun export_html thy spans = - let - val name = Context.theory_name thy; - val parents = - Theory.parents_of thy |> map (fn thy' => - (Url.File (theory_link thy thy'), Context.theory_name thy')); - - 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; - (* hook for consolidated theory *) @@ -113,7 +62,6 @@ val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => - (export_html thy (map #span segments); if exists (Toplevel.is_skipped_proof o #state) segments then () else let @@ -128,7 +76,7 @@ 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));