generate theory HTML in Isabelle/Scala;
discontinued HTML support in Isabelle/ML;
--- 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)
--- 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)
--- 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 =
--- 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;
--- 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)))))))))
}
--- 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*)
--- 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>", "</span>")
- | span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
-
-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 "⇘" ^ "<sub>"),
- ("\<^esub>", hidden "⇙" ^ "</sub>"),
- ("\<^bsup>", hidden "⇗" ^ "<sup>"),
- ("\<^esup>", hidden "⇖" ^ "</sup>")];
- 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 ("<sub>", "</sub>");
-val output_sup = output_markup ("<sup>", "</sup>");
-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 "<span class=\"name\">" "</span>" oo output;
-val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
-val command = enclose "<span class=\"command\">" "</span>" oo output;
-
-
-(* misc *)
-
-fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
-fun href_path path txt = href_name (Url.implode path) txt;
-
-
-(* document *)
-
-fun begin_document symbols title =
- XML.header ^
- "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
- "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
- "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
- "<head>\n" ^
- "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
- "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
- "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
- "</head>\n" ^
- "\n" ^
- "<body>\n" ^
- "<div class=\"head\">" ^
- "<h1>" ^ output symbols title ^ "</h1>\n";
-
-val end_document = "\n</div>\n</body>\n</html>\n";
-
-end;
--- 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
}
--- 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
}
--- 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 ^ "<br/>\n" ^
- (if null Bs then ""
- else
- HTML.keyword symbols "imports" ^ " " ^
- space_implode " " (map (uncurry HTML.href_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
-
-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));