additional tex dump;
authorwenzelm
Sat Feb 05 16:57:02 2000 +0100 (2000-02-05)
changeset 8196ecb9decd38ac
parent 8195 af2575a5c5ae
child 8197 baab8e487fad
additional tex dump;
src/Pure/Isar/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Isar/session.ML	Sat Feb 05 16:54:27 2000 +0100
     1.2 +++ b/src/Pure/Isar/session.ML	Sat Feb 05 16:57:02 2000 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature SESSION =
     1.5  sig
     1.6    val welcome: unit -> string
     1.7 -  val use_dir: bool -> bool -> string -> string -> string -> string -> unit
     1.8 +  val use_dir: bool -> bool -> string -> string -> string -> string -> string -> unit
     1.9    val finish: unit -> unit
    1.10  end;
    1.11  
    1.12 @@ -67,9 +67,10 @@
    1.13         rpath := Some (Url.unpack rpath_str);
    1.14     (!rpath, rpath_str <> ""));
    1.15  
    1.16 -fun use_dir reset info doc parent name rpath_str =
    1.17 +fun use_dir reset info doc parent name dump rpath_str =
    1.18    (init reset parent name;
    1.19 -   Present.init info doc (path ()) name (get_rpath rpath_str);
    1.20 +   Present.init info doc (path ()) name
    1.21 +     (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
    1.22     File.symbol_use root_file;
    1.23     finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    1.24  
     2.1 --- a/src/Pure/Thy/present.ML	Sat Feb 05 16:54:27 2000 +0100
     2.2 +++ b/src/Pure/Thy/present.ML	Sat Feb 05 16:57:02 2000 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      ID:         $Id$
     2.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     2.6  
     2.7 -Theory presentation (HTML, graph files, simple LaTeX documents).
     2.8 +Theory presentation (HTML, graph files, (PDF)LaTeX documents).
     2.9  *)
    2.10  
    2.11  signature BASIC_PRESENT =
    2.12 @@ -13,7 +13,7 @@
    2.13  signature PRESENT =
    2.14  sig
    2.15    include BASIC_PRESENT
    2.16 -  val init: bool -> string -> string list -> string -> Url.T option * bool -> unit
    2.17 +  val init: bool -> string -> string list -> string -> Path.T option -> Url.T option * bool -> unit
    2.18    val finish: unit -> unit
    2.19    val init_theory: string -> unit
    2.20    val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
    2.21 @@ -53,7 +53,7 @@
    2.22  val graph_path = Path.ext "graph" o Path.basic;
    2.23  val index_path = Path.basic "index.html";
    2.24  val doc_path = Path.basic "document";
    2.25 -val doc_index_path = tex_path "session";
    2.26 +val doc_indexN = "session";
    2.27  
    2.28  val session_path = Path.basic ".session";
    2.29  val session_entries_path = Path.unpack ".session/entries";
    2.30 @@ -216,13 +216,13 @@
    2.31  
    2.32  type session_info =
    2.33    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    2.34 -    doc_format: string, doc_prefix: Path.T option, graph_path: Path.T, all_graph_path: Path.T,
    2.35 -    remote_path: Url.T option};
    2.36 +    doc_format: string, doc_prefixes: (Path.T * Path.T option) option, graph_path: Path.T,
    2.37 +    all_graph_path: Path.T, remote_path: Url.T option};
    2.38  
    2.39 -fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefix,
    2.40 +fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefixes,
    2.41      graph_path, all_graph_path, remote_path) =
    2.42    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    2.43 -    doc_format = doc_format, doc_prefix = doc_prefix, graph_path = graph_path,
    2.44 +    doc_format = doc_format, doc_prefixes = doc_prefixes, graph_path = graph_path,
    2.45      all_graph_path = all_graph_path, remote_path = remote_path}: session_info;
    2.46  
    2.47  
    2.48 @@ -269,8 +269,8 @@
    2.49    if File.exists inpath then (File.copy inpath outpath; true)
    2.50    else false;
    2.51  
    2.52 -fun init false _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
    2.53 -  | init true doc path name (remote_path, first_time) =
    2.54 +fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
    2.55 +  | init true doc path name dump_path (remote_path, first_time) =
    2.56        let
    2.57          val parent_name = name_of_session (take (length path - 1, path));
    2.58          val session_name = name_of_session path;
    2.59 @@ -279,9 +279,9 @@
    2.60          val out_path = Path.expand output_path;
    2.61          val html_prefix = Path.append out_path sess_prefix;
    2.62  
    2.63 -        val (doc_prefix, document_path) =
    2.64 +        val (doc_prefixes, document_path) =
    2.65            if doc = "" then (None, None)
    2.66 -          else (Some (Path.append html_prefix doc_path), Some (Path.ext doc doc_path));
    2.67 +          else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
    2.68  
    2.69          val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
    2.70          val graph_path = Path.append graph_prefix (Path.basic "session.graph");
    2.71 @@ -314,11 +314,11 @@
    2.72        in
    2.73          File.mkdir (Path.append html_prefix session_path);
    2.74          File.write (Path.append html_prefix session_entries_path) "";
    2.75 -        if is_some doc_prefix then File.copy_all doc_path html_prefix else ();
    2.76 +        if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
    2.77          seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt)
    2.78            (HTML.applet_pages session_name codebase graph_up_lnk (length path = 1));
    2.79          session_info := Some (make_session_info (name, parent_name, session_name, path,
    2.80 -          html_prefix, doc, doc_prefix, graph_path, all_graph_path, remote_path));
    2.81 +          html_prefix, doc, doc_prefixes, graph_path, all_graph_path, remote_path));
    2.82          browser_info := initial_browser_info remote_path all_graph_path path;
    2.83          add_html_index index_text
    2.84        end;
    2.85 @@ -330,19 +330,25 @@
    2.86    let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
    2.87    in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
    2.88  
    2.89 +fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
    2.90 +
    2.91 +fun write_texes src name (path, None) = write_tex src name path
    2.92 +  | write_texes src name (path, Some path') = (write_tex src name path; write_tex src name path');
    2.93 +
    2.94 +
    2.95  fun finish () = with_session ()
    2.96 -    (fn {name, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, path, ...} =>
    2.97 +    (fn {name, html_prefix, doc_format, doc_prefixes, graph_path, all_graph_path, path, ...} =>
    2.98    let
    2.99      val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
   2.100  
   2.101      fun finish_node (a, {tex_source, html_source = _, html}) =
   2.102 -     (doc_prefix |> apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source);
   2.103 +     (doc_prefixes |> apsome (write_texes tex_source a);
   2.104        Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   2.105    in
   2.106      seq finish_node (Symtab.dest theories);
   2.107      Buffer.write (Path.append html_prefix pre_index_path) html_index;
   2.108 -    doc_prefix |> apsome (fn p =>
   2.109 -     (Buffer.write (Path.append p doc_index_path) tex_index; isatool_document doc_format p));
   2.110 +    doc_prefixes |> apsome (write_texes tex_index doc_indexN);
   2.111 +    doc_prefixes |> apsome (isatool_document doc_format o #1);
   2.112      put_graph graph graph_path;
   2.113      put_graph all_graph all_graph_path;
   2.114      create_index html_prefix;