src/Pure/Thy/present.ML

clarified bibtex_entries: refer to overall session structure;

(*  Title:      Pure/Thy/present.ML
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen

Theory presentation: HTML and PDF-LaTeX documents.
*)

signature PRESENT =
sig
  val theory_qualifier: theory -> string
  val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
  val finish: unit -> unit
  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
end;

structure Present: PRESENT =
struct


(** paths **)

val html_ext = Path.ext "html";
val html_path = html_ext o Path.basic;
val index_path = Path.basic "index.html";
val readme_html_path = Path.basic "README.html";
val session_graph_path = Path.basic "session_graph.pdf";
val document_path = Path.ext "pdf" o Path.basic;

fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));



(** theory data **)

type browser_info = {chapter: string, name: string};
val empty_browser_info: browser_info = {chapter = "Unsorted", name = "Unknown"};

structure Browser_Info = Theory_Data
(
  type T = browser_info
  val empty = empty_browser_info;
  val extend = I;
  val merge = #1;
);

fun reset_browser_info thy =
  if Browser_Info.get thy = empty_browser_info then NONE
  else SOME (Browser_Info.put empty_browser_info thy);

val _ =
  Theory.setup
   (Theory.at_begin reset_browser_info #>
    Browser_Info.put {chapter = Context.PureN, name = Context.PureN});



(** global browser info state **)

(* type browser_info *)

type browser_info =
 {html_theories: string Symtab.table,
  html_index: (int * string) list};

fun make_browser_info (html_theories, html_index) : browser_info =
  {html_theories = html_theories, html_index = html_index};

val empty_browser_info = make_browser_info (Symtab.empty, []);

fun map_browser_info f {html_theories, html_index} =
  make_browser_info (f (html_theories, html_index));


(* state *)

val browser_info = Synchronized.var "browser_info" empty_browser_info;
fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);

fun update_html name html = change_browser_info (apfst (Symtab.update (name, html)));

fun add_html_index txt = change_browser_info (apsnd (cons txt));



(** global session state **)

(* session_info *)

type session_info =
  {symbols: HTML.symbols, name: string, chapter: string, info_path: Path.T, info: bool,
    verbose: bool, readme: Path.T option};

fun make_session_info
  (symbols, name, chapter, info_path, info, verbose, readme) =
  {symbols = symbols, name = name, chapter = chapter, info_path = info_path, info = info,
    verbose = verbose, readme = readme}: session_info;


(* state *)

val session_info = Unsynchronized.ref (NONE: session_info option);

fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);

val theory_qualifier = Resources.theory_qualifier o Context.theory_long_name;

fun is_session_theory thy =
  (case ! session_info of
    NONE => false
  | SOME {name, ...} => name = theory_qualifier thy);


(** document preparation **)

(* init session *)

fun init symbols info info_path documents (chapter, name) verbose =
  let
    val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;

    val docs =
      (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
        map (fn name => (Url.File (document_path name), name)) documents;
  in
    session_info :=
      SOME (make_session_info (symbols, name, chapter, info_path, info, verbose, readme));
    Synchronized.change browser_info (K empty_browser_info);
    add_html_index (0, HTML.begin_session_index symbols name (Url.File session_graph_path) docs)
  end;


(* finish session -- output all generated text *)

fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;

fun finish () = with_session_info () (fn {name, chapter, info, info_path, verbose, readme, ...} =>
  let
    val {html_theories, html_index} = Synchronized.value browser_info;

    val session_prefix = info_path + Path.basic chapter + Path.basic name;

    fun finish_html (a, html) = File.write (session_prefix + html_path a) html;

    val _ =
      if info then
       (Isabelle_System.make_directory session_prefix;
        File.write_buffer (session_prefix + index_path)
          (index_buffer html_index |> Buffer.add HTML.end_document);
        (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
        Symtab.fold (K o finish_html) html_theories ();
        if verbose
        then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
        else ())
      else ();
  in
    Synchronized.change browser_info (K empty_browser_info);
    session_info := NONE
  end);


(* theory elements *)

fun theory_link (curr_chapter, curr_session) thy =
  let
    val {chapter, name = session, ...} = Browser_Info.get thy;
    val link = html_path (Context.theory_name thy);
  in
    if curr_session = session then SOME link
    else if curr_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)
  end;

fun begin_theory update_time mk_text thy =
  with_session_info thy (fn {symbols, name = session_name, chapter, ...} =>
    let
      val name = Context.theory_name thy;

      val parent_specs =
        Theory.parents_of thy |> map (fn parent =>
          (Option.map Url.File (theory_link (chapter, session_name) parent),
            (Context.theory_name parent)));

      val _ = update_html name (HTML.theory symbols name parent_specs (mk_text ()));

      val _ =
        if is_session_theory thy then
          add_html_index (update_time, HTML.theory_entry symbols (Url.File (html_path name), name))
        else ();
    in thy |> Browser_Info.put {chapter = chapter, name = session_name} end);

end;