refined "document_dump_mode": "all", "tex+sty", "tex";
authorwenzelm
Thu Jul 26 14:29:54 2012 +0200 (2012-07-26)
changeset 48516c5d0f19ef7cb
parent 48515 3e17f343deb5
child 48517 0f8c8ac6cc0e
refined "document_dump_mode": "all", "tex+sty", "tex";
doc-src/ROOT
etc/options
src/Pure/System/build.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/doc-src/ROOT	Thu Jul 26 14:24:27 2012 +0200
     1.2 +++ b/doc-src/ROOT	Thu Jul 26 14:29:54 2012 +0200
     1.3 @@ -1,10 +1,12 @@
     1.4  session Classes! (doc) in "Classes/Thy" = HOL +
     1.5 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
     1.6 +  options [browser_info = false, document = false,
     1.7 +    document_dump = document, document_dump_mode = "tex"]
     1.8    theories [document = false] Setup
     1.9    theories Classes
    1.10  
    1.11  session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
    1.12 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.13 +  options [browser_info = false, document = false,
    1.14 +    document_dump = document, document_dump_mode = "tex",
    1.15      print_mode = "no_brackets,iff"]
    1.16    theories [document = false] Setup
    1.17    theories
    1.18 @@ -17,11 +19,13 @@
    1.19      Further
    1.20  
    1.21  session Functions! (doc) in "Functions/Thy" = HOL +
    1.22 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.23 +  options [browser_info = false, document = false,
    1.24 +    document_dump = document, document_dump_mode = "tex"]
    1.25    theories Functions
    1.26  
    1.27  session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
    1.28 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.29 +  options [browser_info = false, document = false,
    1.30 +    document_dump = document, document_dump_mode = "tex"]
    1.31    theories
    1.32      Eq
    1.33      Integration
    1.34 @@ -35,7 +39,8 @@
    1.35      Tactic
    1.36  
    1.37  session IsarRef (doc) in "IsarRef/Thy" = HOL +
    1.38 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.39 +  options [browser_info = false, document = false,
    1.40 +    document_dump = document, document_dump_mode = "tex",
    1.41      quick_and_dirty]
    1.42    theories
    1.43      Preface
    1.44 @@ -55,17 +60,20 @@
    1.45      ML_Tactic
    1.46  
    1.47  session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
    1.48 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.49 +  options [browser_info = false, document = false,
    1.50 +    document_dump = document, document_dump_mode = "tex",
    1.51      quick_and_dirty]
    1.52    theories HOLCF_Specific
    1.53  
    1.54  session IsarRef (doc) in "IsarRef/Thy" = ZF +
    1.55 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.56 +  options [browser_info = false, document = false,
    1.57 +    document_dump = document, document_dump_mode = "tex",
    1.58      quick_and_dirty]
    1.59    theories ZF_Specific
    1.60  
    1.61  session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
    1.62 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.63 +  options [browser_info = false, document = false,
    1.64 +    document_dump = document, document_dump_mode = "tex",
    1.65      threads = 1]  (* FIXME *)
    1.66    theories [document_dump = ""]
    1.67      "~~/src/HOL/Library/LaTeXsugar"
    1.68 @@ -73,18 +81,21 @@
    1.69    theories Sugar
    1.70  
    1.71  session Locales! (doc) in "Locales/Locales" = HOL +
    1.72 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.73 +  options [browser_info = false, document = false,
    1.74 +    document_dump = document, document_dump_mode = "tex"]
    1.75    theories
    1.76      Examples1
    1.77      Examples2
    1.78      Examples3
    1.79  
    1.80  session Main! (doc) in "Main/Docs" = HOL +
    1.81 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.82 +  options [browser_info = false, document = false,
    1.83 +    document_dump = document, document_dump_mode = "tex"]
    1.84    theories Main_Doc
    1.85  
    1.86  session ProgProve! (doc) in "ProgProve/Thys" = HOL +
    1.87 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
    1.88 +  options [browser_info = false, document = false,
    1.89 +    document_dump = document, document_dump_mode = "tex",
    1.90      show_question_marks = false]
    1.91    theories
    1.92      Basics
    1.93 @@ -95,7 +106,8 @@
    1.94      Isar
    1.95  
    1.96  session System! (doc) in "System/Thy" = Pure +
    1.97 -  options [browser_info = false, document = false, document_dump = document, document_dump_only]
    1.98 +  options [browser_info = false, document = false,
    1.99 +    document_dump = document, document_dump_mode = "tex"]
   1.100    theories
   1.101      Basics
   1.102      Interfaces
   1.103 @@ -106,7 +118,8 @@
   1.104  (* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
   1.105  
   1.106  session examples (doc) in "ZF" = ZF +
   1.107 -  options [browser_info = false, document = false, document_dump = document, document_dump_only,
   1.108 +  options [browser_info = false, document = false,
   1.109 +    document_dump = document, document_dump_mode = "tex",
   1.110      print_mode = "brackets"]
   1.111    theories
   1.112      IFOL_examples
     2.1 --- a/etc/options	Thu Jul 26 14:24:27 2012 +0200
     2.2 +++ b/etc/options	Thu Jul 26 14:29:54 2012 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  declare document_variants : string = "outline=/proof,/ML"
     2.5  declare document_graph : bool = false
     2.6  declare document_dump : string = ""
     2.7 -declare document_dump_only : bool = false
     2.8 +declare document_dump_mode : string = "all"
     2.9  declare no_document : bool = false
    2.10  
    2.11  declare threads : int = 0
     3.1 --- a/src/Pure/System/build.ML	Thu Jul 26 14:24:27 2012 +0200
     3.2 +++ b/src/Pure/System/build.ML	Thu Jul 26 14:29:54 2012 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4          (Options.bool options "document_graph")
     3.5          (space_explode ":" (Options.string options "document_variants"))
     3.6          parent_base_name base_name
     3.7 -        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
     3.8 +        (Options.string options "document_dump", Options.string options "document_dump_mode")
     3.9          "" verbose;
    3.10      val _ = Session.with_timing name timing (List.app use_theories) theories;
    3.11      val _ = Session.finish ();
     4.1 --- a/src/Pure/System/session.ML	Thu Jul 26 14:24:27 2012 +0200
     4.2 +++ b/src/Pure/System/session.ML	Thu Jul 26 14:29:54 2012 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4    val welcome: unit -> string
     4.5    val finish: unit -> unit
     4.6    val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
     4.7 -    string -> string -> bool * string -> string -> bool -> unit
     4.8 +    string -> string -> string * string -> string -> bool -> unit
     4.9    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    4.10    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    4.11      string -> bool -> string list -> string -> string -> bool * string ->
    4.12 @@ -85,17 +85,6 @@
    4.13  
    4.14  (* use_dir *)
    4.15  
    4.16 -fun get_rpath rpath =
    4.17 -  (if rpath = "" then () else
    4.18 -     if is_some (! remote_path) then
    4.19 -       error "Path for remote theory browsing information may only be set once"
    4.20 -     else
    4.21 -       remote_path := SOME (Url.explode rpath);
    4.22 -   (! remote_path, rpath <> ""));
    4.23 -
    4.24 -fun dumping (_, "") = NONE
    4.25 -  | dumping (cp, path) = SOME (cp, Path.explode path);
    4.26 -
    4.27  fun with_timing _ false f x = f x
    4.28    | with_timing item true f x =
    4.29        let
    4.30 @@ -110,17 +99,32 @@
    4.31              Timing.message timing ^ ", factor " ^ factor ^ ")\n");
    4.32        in y end;
    4.33  
    4.34 -fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
    4.35 +fun get_rpath rpath =
    4.36 +  (if rpath = "" then () else
    4.37 +     if is_some (! remote_path) then
    4.38 +       error "Path for remote theory browsing information may only be set once"
    4.39 +     else
    4.40 +       remote_path := SOME (Url.explode rpath);
    4.41 +   (! remote_path, rpath <> ""));
    4.42 +
    4.43 +fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
    4.44   (init_name reset parent name;
    4.45    Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
    4.46 -    (path ()) name (dumping dump) (get_rpath rpath) verbose
    4.47 +    (path ()) name doc_dump (get_rpath rpath) verbose
    4.48      (map Thy_Info.get_theory (Thy_Info.get_names ())));
    4.49  
    4.50 +local
    4.51 +
    4.52 +fun doc_dump (cp, dump) = (if cp then "all" else "tex+sty", dump);
    4.53 +
    4.54 +in
    4.55 +
    4.56  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    4.57      name dump rpath level timing verbose max_threads trace_threads
    4.58      parallel_proofs parallel_proofs_threshold =
    4.59    ((fn () =>
    4.60 -     (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
    4.61 +     (init build reset info info_path doc doc_graph doc_variants parent name
    4.62 +        (doc_dump dump) rpath verbose;
    4.63        with_timing item timing use root;
    4.64        finish ()))
    4.65      |> Unsynchronized.setmp Proofterm.proofs level
    4.66 @@ -134,3 +138,5 @@
    4.67    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    4.68  
    4.69  end;
    4.70 +
    4.71 +end;
     5.1 --- a/src/Pure/Thy/present.ML	Thu Jul 26 14:24:27 2012 +0200
     5.2 +++ b/src/Pure/Thy/present.ML	Thu Jul 26 14:29:54 2012 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     5.5     path: string, parents: string list} list -> unit
     5.6    val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     5.7 -    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
     5.8 +    string -> string * string -> Url.T option * bool -> bool ->
     5.9      theory list -> unit  (*not thread-safe!*)
    5.10    val finish: unit -> unit  (*not thread-safe!*)
    5.11    val init_theory: string -> unit
    5.12 @@ -210,15 +210,15 @@
    5.13  type session_info =
    5.14    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    5.15      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
    5.16 -    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
    5.17 +    doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
    5.18      readme: Path.T option};
    5.19  
    5.20  fun make_session_info
    5.21    (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
    5.22 -    dump_prefix, remote_path, verbose, readme) =
    5.23 +    doc_dump, remote_path, verbose, readme) =
    5.24    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    5.25      info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
    5.26 -    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
    5.27 +    doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
    5.28      readme = readme}: session_info;
    5.29  
    5.30  
    5.31 @@ -273,9 +273,9 @@
    5.32  
    5.33  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    5.34  
    5.35 -fun init build info info_path doc doc_graph doc_variants path name dump_prefix
    5.36 -    (remote_path, first_time) verbose thys =
    5.37 -  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
    5.38 +fun init build info info_path doc doc_graph doc_variants path name
    5.39 +    (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
    5.40 +  if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
    5.41      (browser_info := empty_browser_info; session_info := NONE)
    5.42    else
    5.43      let
    5.44 @@ -309,7 +309,7 @@
    5.45      in
    5.46        session_info :=
    5.47          SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    5.48 -          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
    5.49 +          info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
    5.50        browser_info := init_browser_info remote_path path thys;
    5.51        add_html_index (0, index_text)
    5.52      end;
    5.53 @@ -360,32 +360,34 @@
    5.54  
    5.55  fun finish () =
    5.56    session_default () (fn {name, info, html_prefix, doc_format,
    5.57 -    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
    5.58 +    doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
    5.59    let
    5.60      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    5.61      val thys = Symtab.dest theories;
    5.62      val parent_html_prefix = Path.append html_prefix Path.parent;
    5.63  
    5.64 -    fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
    5.65      fun finish_html (a, {html, ...}: theory_info) =
    5.66        File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
    5.67  
    5.68      val sorted_graph = sorted_index graph;
    5.69      val opt_graphs =
    5.70 -      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
    5.71 +      if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then
    5.72          SOME (isabelle_browser sorted_graph)
    5.73        else NONE;
    5.74  
    5.75 -    fun prepare_sources cp path =
    5.76 -     (Isabelle_System.mkdirs path;
    5.77 -      if cp then Isabelle_System.copy_dir document_path path else ();
    5.78 -      Isabelle_System.isabelle_tool "latex"
    5.79 -        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    5.80 +    fun prepare_sources doc_dir doc_mode =
    5.81 +     (Isabelle_System.mkdirs doc_dir;
    5.82 +      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
    5.83 +      else if doc_mode = "tex+sty" then
    5.84 +        ignore (Isabelle_System.isabelle_tool "latex"
    5.85 +          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    5.86 +      else if doc_mode = "tex" then ()
    5.87 +      else error ("Illegal document dump mode: " ^ quote doc_mode);
    5.88        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    5.89 -        (File.write (Path.append path graph_pdf_path) pdf;
    5.90 -          File.write (Path.append path graph_eps_path) eps));
    5.91 -      write_tex_index tex_index path;
    5.92 -      List.app (finish_tex path) thys);
    5.93 +        (File.write (Path.append doc_dir graph_pdf_path) pdf;
    5.94 +          File.write (Path.append doc_dir graph_eps_path) eps));
    5.95 +      write_tex_index tex_index doc_dir;
    5.96 +      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
    5.97      val _ =
    5.98        if info then
    5.99         (Isabelle_System.mkdirs (Path.append html_prefix session_path);
   5.100 @@ -407,16 +409,22 @@
   5.101        else ();
   5.102  
   5.103      val _ =
   5.104 -      (case dump_prefix of NONE => () | SOME (cp, path) =>
   5.105 -       (prepare_sources cp path;
   5.106 -        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
   5.107 -        else ()));
   5.108 +      if dump_prefix = "" then ()
   5.109 +      else
   5.110 +        let
   5.111 +          val path = Path.explode dump_prefix;
   5.112 +          val _ = prepare_sources path dump_mode;
   5.113 +        in
   5.114 +          if verbose then
   5.115 +            Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
   5.116 +          else ()
   5.117 +        end;
   5.118  
   5.119      val doc_paths =
   5.120        documents |> Par_List.map (fn (name, tags) =>
   5.121          let
   5.122            val path = Path.append html_prefix (Path.basic name);
   5.123 -          val _ = prepare_sources true path;
   5.124 +          val _ = prepare_sources path "all";
   5.125          in isabelle_document true doc_format name tags path html_prefix end);
   5.126      val _ =
   5.127        if verbose then