eliminated redundant doc_prefix1;
authorwenzelm
Sun Mar 20 19:34:18 2011 +0100 (2011-03-20)
changeset 420072142883ec29f
parent 42006 7eecd020e367
child 42008 7423e833a880
eliminated redundant doc_prefix1;
tuned;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 19:10:09 2011 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 19:34:18 2011 +0100
     1.3 @@ -215,16 +215,16 @@
     1.4  type session_info =
     1.5    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
     1.6      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
     1.7 -    doc_prefix1: (Path.T * Path.T) option, dump_prefix: (bool * Path.T) option,
     1.8 -    remote_path: Url.T option, verbose: bool, readme: Path.T option};
     1.9 +    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
    1.10 +    readme: Path.T option};
    1.11  
    1.12  fun make_session_info
    1.13    (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
    1.14 -    doc_prefix1, dump_prefix, remote_path, verbose, readme) =
    1.15 +    dump_prefix, remote_path, verbose, readme) =
    1.16    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    1.17      info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
    1.18 -    doc_prefix1 = doc_prefix1, dump_prefix = dump_prefix, remote_path = remote_path,
    1.19 -    verbose = verbose, readme = readme}: session_info;
    1.20 +    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
    1.21 +    readme = readme}: session_info;
    1.22  
    1.23  
    1.24  (* state *)
    1.25 @@ -290,16 +290,15 @@
    1.26        val sess_prefix = Path.make path;
    1.27        val html_prefix = Path.append (Path.expand output_path) sess_prefix;
    1.28  
    1.29 -      val (doc_prefix1, documents) =
    1.30 -        if doc = "" then (NONE, [])
    1.31 +      val documents =
    1.32 +        if doc = "" then []
    1.33          else if not (can File.check_dir document_path) then
    1.34 -          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
    1.35 -            (NONE, []))
    1.36 -        else (SOME (Path.append html_prefix document_path, html_prefix),
    1.37 -          read_variants doc_variants);
    1.38 +          (if verbose then Output.raw_stderr "Warning: missing document directory\n" else (); [])
    1.39 +        else read_variants doc_variants;
    1.40  
    1.41        val parent_index_path = Path.append Path.parent index_path;
    1.42 -      val index_up_lnk = if first_time then
    1.43 +      val index_up_lnk =
    1.44 +        if first_time then
    1.45            Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
    1.46          else Url.File parent_index_path;
    1.47        val readme =
    1.48 @@ -309,12 +308,13 @@
    1.49  
    1.50        val docs =
    1.51          (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
    1.52 -        map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
    1.53 +          map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
    1.54        val index_text = HTML.begin_index (index_up_lnk, parent_name)
    1.55          (Url.File index_path, session_name) docs (Url.explode "medium.html");
    1.56      in
    1.57 -      session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    1.58 -        info, doc, doc_graph, documents, doc_prefix1, dump_prefix, remote_path, verbose, readme));
    1.59 +      session_info :=
    1.60 +        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    1.61 +          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
    1.62        browser_info := init_browser_info remote_path path thys;
    1.63        add_html_index (0, index_text)
    1.64      end);
    1.65 @@ -366,8 +366,8 @@
    1.66  
    1.67  
    1.68  fun finish () = CRITICAL (fn () =>
    1.69 -    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
    1.70 -      documents, doc_prefix1, dump_prefix, path, verbose, readme, ...} =>
    1.71 +    with_session () (fn {name, info, html_prefix, doc_format, doc_graph, documents,
    1.72 +      dump_prefix, path, verbose, readme, ...} =>
    1.73    let
    1.74      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    1.75      val thys = Symtab.dest theories;
    1.76 @@ -379,7 +379,7 @@
    1.77  
    1.78      val sorted_graph = sorted_index graph;
    1.79      val opt_graphs =
    1.80 -      if doc_graph andalso (is_some doc_prefix1 orelse is_some dump_prefix) then
    1.81 +      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
    1.82          SOME (isabelle_browser sorted_graph)
    1.83        else NONE;
    1.84  
    1.85 @@ -393,38 +393,43 @@
    1.86            File.write (Path.append path graph_eps_path) eps));
    1.87        write_tex_index tex_index path;
    1.88        List.app (finish_tex path) thys);
    1.89 +    val _ =
    1.90 +      if info then
    1.91 +       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
    1.92 +        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
    1.93 +        File.write (Path.append html_prefix session_entries_path) "";
    1.94 +        create_index html_prefix;
    1.95 +        if length path > 1 then update_index parent_html_prefix name else ();
    1.96 +        (case readme of NONE => () | SOME path => File.copy path html_prefix);
    1.97 +        write_graph sorted_graph (Path.append html_prefix graph_path);
    1.98 +        Isabelle_System.isabelle_tool "browser" "-b";
    1.99 +        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
   1.100 +        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
   1.101 +          (HTML.applet_pages name (Url.File index_path, name));
   1.102 +        File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
   1.103 +        List.app finish_html thys;
   1.104 +        List.app (uncurry File.write) files;
   1.105 +        if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
   1.106 +        else ())
   1.107 +      else ();
   1.108 +
   1.109 +    val _ =
   1.110 +      (case dump_prefix of NONE => () | SOME (cp, path) =>
   1.111 +       (prepare_sources cp path;
   1.112 +        if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n")
   1.113 +        else ()));
   1.114 +
   1.115 +    val doc_paths =
   1.116 +      documents |> map (fn (name, tags) =>
   1.117 +        let
   1.118 +          val path = Path.append html_prefix document_path;
   1.119 +          val _ = prepare_sources true path;
   1.120 +        in isabelle_document true doc_format name tags path html_prefix end);
   1.121 +    val _ =
   1.122 +      if verbose then
   1.123 +        doc_paths |> List.app (fn doc => Output.raw_stderr ("Document at " ^ show_path doc ^ "\n"))
   1.124 +      else ();
   1.125    in
   1.126 -    if info then
   1.127 -     (Isabelle_System.mkdirs (Path.append html_prefix session_path);
   1.128 -      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
   1.129 -      File.write (Path.append html_prefix session_entries_path) "";
   1.130 -      create_index html_prefix;
   1.131 -      if length path > 1 then update_index parent_html_prefix name else ();
   1.132 -      (case readme of NONE => () | SOME path => File.copy path html_prefix);
   1.133 -      write_graph sorted_graph (Path.append html_prefix graph_path);
   1.134 -      Isabelle_System.isabelle_tool "browser" "-b";
   1.135 -      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
   1.136 -      List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
   1.137 -        (HTML.applet_pages name (Url.File index_path, name));
   1.138 -      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
   1.139 -      List.app finish_html thys;
   1.140 -      List.app (uncurry File.write) files;
   1.141 -      if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
   1.142 -    else ();
   1.143 -
   1.144 -    (case dump_prefix of NONE => () | SOME (cp, path) =>
   1.145 -     (prepare_sources cp path;
   1.146 -      if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
   1.147 -
   1.148 -    (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
   1.149 -      documents |> List.app (fn (name, tags) =>
   1.150 -       let
   1.151 -         val _ = prepare_sources true path;
   1.152 -         val doc_path = isabelle_document true doc_format name tags path result_path;
   1.153 -       in
   1.154 -         if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
   1.155 -       end));
   1.156 -
   1.157      browser_info := empty_browser_info;
   1.158      session_info := NONE
   1.159    end));