--- a/src/Pure/Thy/html.ML Sat Nov 16 20:20:09 2013 +0100
+++ b/src/Pure/Thy/html.ML Sat Nov 16 21:18:31 2013 +0100
@@ -23,8 +23,7 @@
val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
val applet_pages: string -> Url.T * string -> (string * string) list
val theory_entry: Url.T * string -> text
- val theory_source: text -> text
- val begin_theory: string -> (Url.T option * string) list -> text -> text
+ val theory: string -> (Url.T option * string) list -> text -> text
end;
structure HTML: HTML =
@@ -320,13 +319,12 @@
(* theory *)
-val theory_source = enclose
- "\n</div>\n<div class=\"source\">\n<pre>"
- "</pre>\n";
-
-fun begin_theory A Bs body =
- begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A ^ "<br/>\n" ^
+fun theory A Bs txt =
+ begin_document ("Theory " ^ A) ^ "\n" ^
+ command "theory" ^ " " ^ name A ^ "<br/>\n" ^
keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
- "<br/>\n" ^ body;
+ "<br/>\n" ^
+ enclose "\n</div>\n<div class=\"source\">\n<pre>" "</pre>\n" txt ^
+ end_document;
end;