src/Pure/Thy/present.ML
changeset 48516 c5d0f19ef7cb
parent 48445 cb4136e4cabf
child 48543 93b558e05f21
     1.1 --- a/src/Pure/Thy/present.ML	Thu Jul 26 14:24:27 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Jul 26 14:29:54 2012 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     1.5     path: string, parents: string list} list -> unit
     1.6    val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     1.7 -    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
     1.8 +    string -> string * string -> Url.T option * bool -> bool ->
     1.9      theory list -> unit  (*not thread-safe!*)
    1.10    val finish: unit -> unit  (*not thread-safe!*)
    1.11    val init_theory: string -> unit
    1.12 @@ -210,15 +210,15 @@
    1.13  type session_info =
    1.14    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    1.15      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
    1.16 -    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
    1.17 +    doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
    1.18      readme: Path.T option};
    1.19  
    1.20  fun make_session_info
    1.21    (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
    1.22 -    dump_prefix, remote_path, verbose, readme) =
    1.23 +    doc_dump, remote_path, verbose, readme) =
    1.24    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    1.25      info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
    1.26 -    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
    1.27 +    doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
    1.28      readme = readme}: session_info;
    1.29  
    1.30  
    1.31 @@ -273,9 +273,9 @@
    1.32  
    1.33  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    1.34  
    1.35 -fun init build info info_path doc doc_graph doc_variants path name dump_prefix
    1.36 -    (remote_path, first_time) verbose thys =
    1.37 -  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
    1.38 +fun init build info info_path doc doc_graph doc_variants path name
    1.39 +    (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
    1.40 +  if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
    1.41      (browser_info := empty_browser_info; session_info := NONE)
    1.42    else
    1.43      let
    1.44 @@ -309,7 +309,7 @@
    1.45      in
    1.46        session_info :=
    1.47          SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    1.48 -          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
    1.49 +          info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
    1.50        browser_info := init_browser_info remote_path path thys;
    1.51        add_html_index (0, index_text)
    1.52      end;
    1.53 @@ -360,32 +360,34 @@
    1.54  
    1.55  fun finish () =
    1.56    session_default () (fn {name, info, html_prefix, doc_format,
    1.57 -    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
    1.58 +    doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
    1.59    let
    1.60      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    1.61      val thys = Symtab.dest theories;
    1.62      val parent_html_prefix = Path.append html_prefix Path.parent;
    1.63  
    1.64 -    fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
    1.65      fun finish_html (a, {html, ...}: theory_info) =
    1.66        File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
    1.67  
    1.68      val sorted_graph = sorted_index graph;
    1.69      val opt_graphs =
    1.70 -      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
    1.71 +      if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then
    1.72          SOME (isabelle_browser sorted_graph)
    1.73        else NONE;
    1.74  
    1.75 -    fun prepare_sources cp path =
    1.76 -     (Isabelle_System.mkdirs path;
    1.77 -      if cp then Isabelle_System.copy_dir document_path path else ();
    1.78 -      Isabelle_System.isabelle_tool "latex"
    1.79 -        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    1.80 +    fun prepare_sources doc_dir doc_mode =
    1.81 +     (Isabelle_System.mkdirs doc_dir;
    1.82 +      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
    1.83 +      else if doc_mode = "tex+sty" then
    1.84 +        ignore (Isabelle_System.isabelle_tool "latex"
    1.85 +          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    1.86 +      else if doc_mode = "tex" then ()
    1.87 +      else error ("Illegal document dump mode: " ^ quote doc_mode);
    1.88        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.89 -        (File.write (Path.append path graph_pdf_path) pdf;
    1.90 -          File.write (Path.append path graph_eps_path) eps));
    1.91 -      write_tex_index tex_index path;
    1.92 -      List.app (finish_tex path) thys);
    1.93 +        (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.94 +          File.write (Path.append doc_dir graph_eps_path) eps));
    1.95 +      write_tex_index tex_index doc_dir;
    1.96 +      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
    1.97      val _ =
    1.98        if info then
    1.99         (Isabelle_System.mkdirs (Path.append html_prefix session_path);
   1.100 @@ -407,16 +409,22 @@
   1.101        else ();
   1.102  
   1.103      val _ =
   1.104 -      (case dump_prefix of NONE => () | SOME (cp, path) =>
   1.105 -       (prepare_sources cp path;
   1.106 -        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
   1.107 -        else ()));
   1.108 +      if dump_prefix = "" then ()
   1.109 +      else
   1.110 +        let
   1.111 +          val path = Path.explode dump_prefix;
   1.112 +          val _ = prepare_sources path dump_mode;
   1.113 +        in
   1.114 +          if verbose then
   1.115 +            Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
   1.116 +          else ()
   1.117 +        end;
   1.118  
   1.119      val doc_paths =
   1.120        documents |> Par_List.map (fn (name, tags) =>
   1.121          let
   1.122            val path = Path.append html_prefix (Path.basic name);
   1.123 -          val _ = prepare_sources true path;
   1.124 +          val _ = prepare_sources path "all";
   1.125          in isabelle_document true doc_format name tags path html_prefix end);
   1.126      val _ =
   1.127        if verbose then