diff --git a/src/Pure/Thy/html.ML b/src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML +++ b/src/Pure/Thy/html.ML @@ -1,146 +1,142 @@ (* 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 href_opt_path: Url.T option -> 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; -fun href_opt_path NONE txt = txt - | href_opt_path (SOME p) txt = href_path p 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 --git a/src/Pure/Thy/present.ML b/src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML +++ b/src/Pure/Thy/present.ML @@ -1,75 +1,76 @@ (* Title: Pure/Thy/present.ML Author: Makarius Theory presentation: HTML and LaTeX documents. *) signature PRESENT = sig 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 (** artefact names **) 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 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) + 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" ^ - HTML.keyword symbols "imports" ^ " " ^ - space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^ - "
\n\n\n
\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' => - (Option.map Url.File (theory_link thy thy'), Context.theory_name 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; end;