39 fun theory_link thy thy' = |
39 fun theory_link thy thy' = |
40 let |
40 let |
41 val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy'); |
41 val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy'); |
42 val link = html_name thy'; |
42 val link = html_name thy'; |
43 in |
43 in |
44 if session = session' then SOME link |
44 if session = session' then link |
45 else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link) |
45 else if chapter = chapter' then Path.parent + Path.basic session' + link |
46 else if chapter' = Context.PureN then NONE |
46 else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link |
47 else SOME (Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link) |
|
48 end; |
47 end; |
49 |
48 |
50 fun theory_document symbols A Bs body = |
49 fun theory_document symbols A Bs body = |
51 HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^ |
50 HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^ |
52 HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^ |
51 HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^ |
53 HTML.keyword symbols "imports" ^ " " ^ |
52 (if null Bs then "" |
54 space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^ |
53 else |
55 "<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" :: |
54 HTML.keyword symbols "imports" ^ " " ^ |
|
55 space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^ |
|
56 "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" :: |
56 body @ ["</pre>\n", HTML.end_document]; |
57 body @ ["</pre>\n", HTML.end_document]; |
57 |
58 |
58 in |
59 in |
59 |
60 |
60 fun export_html thy spans = |
61 fun export_html thy spans = |
61 let |
62 let |
62 val name = Context.theory_name thy; |
63 val name = Context.theory_name thy; |
63 val parents = |
64 val parents = |
64 Theory.parents_of thy |> map (fn thy' => |
65 Theory.parents_of thy |> map (fn thy' => |
65 (Option.map Url.File (theory_link thy thy'), Context.theory_name thy')); |
66 (Url.File (theory_link thy thy'), Context.theory_name thy')); |
66 |
67 |
67 val symbols = Resources.html_symbols (); |
68 val symbols = Resources.html_symbols (); |
68 val keywords = Thy_Header.get_keywords thy; |
69 val keywords = Thy_Header.get_keywords thy; |
69 val body = map (HTML.present_span symbols keywords) spans; |
70 val body = map (HTML.present_span symbols keywords) spans; |
70 val html = XML.blob (theory_document symbols name parents body); |
71 val html = XML.blob (theory_document symbols name parents body); |