src/Pure/Thy/present.ML

 *)
 
 signature BASIC_PRESENT =
 sig
   val no_document: ('a -> 'b) -> 'a -> 'b
-  val section: string -> unit
 end;
 
 signature PRESENT =
 sig
   include BASIC_PRESENT

    path: string, parents: string list} list -> unit
   val init: bool -> bool -> string -> bool -> string list -> string list ->
     string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit
   val finish: unit -> unit
   val init_theory: string -> unit
-  val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
+  val theory_source: string -> (unit -> HTML.text) -> unit
   val theory_output: string -> string -> unit
   val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
-  val add_hook: (string -> (string * thm list) list -> unit) -> unit
-  val results: string -> (string * thm list) list -> unit
-  val theorem: string -> thm -> unit
-  val theorems: string -> thm list -> unit
-  val chapter: string -> unit
-  val subsection: string -> unit
-  val subsubsection: string -> unit
   val drafts: string -> Path.T list -> Path.T
 end;
 
 structure Present: PRESENT =
 struct

   File.write (Path.append dir session_entries_path) (cat_lines entries);
 
 
 fun create_index dir =
   File.read (Path.append dir pre_index_path) ^
-    session_entries (get_entries dir) ^ HTML.end_index
+    session_entries (get_entries dir) ^ HTML.end_document
   |> File.write (Path.append dir index_path);
 
 fun update_index dir name = CRITICAL (fn () =>
   (case try get_entries dir of
     NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))

     val thys = Symtab.dest theories;
     val parent_html_prefix = Path.append html_prefix Path.parent;
 
     fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
     fun finish_html (a, {html, ...}: theory_info) =
-      Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
+      Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
       if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
         SOME (isatool_browser sorted_graph)

 
 (* theory elements *)
 
 fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
 
-fun verbatim_source name mk_text =
-  with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
+fun theory_source name mk_text =
+  with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
 
 fun theory_output name s =
   with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
 
 

     add_graph_entry (update_time, entry);
     add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (update_time, Latex.theory_entry name);
     put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
   end);
-
-
-val hooks = ref ([]: (string -> (string * thm list) list -> unit) list);
-fun add_hook f = CRITICAL (fn () => change hooks (cons f));
-
-fun results k xs =
- (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks);
-  with_session () (fn _ => with_context add_html
-    (HTML.results (ML_Context.the_local_context ()) k xs)));
-
-fun theorem a th = results Thm.theoremK [(a, [th])];
-fun theorems a ths = results Thm.theoremK [(a, ths)];
-fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
-fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
-fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
-fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
 
 
 
 (** draft document output **)