isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
authorwenzelm
Sun Nov 18 19:01:30 2012 +0100 (2012-11-18)
changeset 5012197d2b77313a0
parent 50120 245f5947233c
child 50122 7ae7efef5ad8
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
always generate sty files, as before c5d0f19ef7cb;
etc/options
src/Pure/System/build.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/etc/options	Sun Nov 18 16:31:41 2012 +0100
     1.2 +++ b/etc/options	Sun Nov 18 19:01:30 2012 +0100
     1.3 @@ -13,10 +13,6 @@
     1.4    -- "option alternative document variants (separated by colons)"
     1.5  option document_graph : bool = false
     1.6    -- "generate session graph image for document"
     1.7 -option document_dump : string = ""
     1.8 -  -- "dump generated document sources into given directory"
     1.9 -option document_dump_mode : string = "all"
    1.10 -  -- "specific document dump mode: all, tex, tex+sty"
    1.11  
    1.12  option show_question_marks : bool = true
    1.13    -- "show leading question mark of schematic variables"
     2.1 --- a/src/Pure/System/build.ML	Sun Nov 18 16:31:41 2012 +0100
     2.2 +++ b/src/Pure/System/build.ML	Sun Nov 18 19:01:30 2012 +0100
     2.3 @@ -15,8 +15,7 @@
     2.4  local
     2.5  
     2.6  fun no_document options =
     2.7 -  (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
     2.8 -  (Options.string options "document_dump" = "");
     2.9 +  (case Options.string options "document" of "" => true | "false" => true | _ => false);
    2.10  
    2.11  fun use_thys options =
    2.12    Thy_Info.use_thys
    2.13 @@ -73,11 +72,6 @@
    2.14          | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    2.15  
    2.16        val _ =
    2.17 -        if Options.string options "document_dump" = "" then ()
    2.18 -        else
    2.19 -          Output.physical_stderr
    2.20 -            "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n";
    2.21 -      val _ =
    2.22          Session.init do_output false
    2.23            (Options.bool options "browser_info") browser_info
    2.24            (Options.string options "document")
    2.25 @@ -85,9 +79,8 @@
    2.26            (Options.string options "document_output")
    2.27            document_variants
    2.28            parent_name name
    2.29 -          (Options.string options "document_dump",
    2.30 -            Present.dump_mode (Options.string options "document_dump_mode"))
    2.31 -          "" verbose;
    2.32 +          (false, "") ""
    2.33 +          verbose;
    2.34  
    2.35        val res1 =
    2.36          theories |>
     3.1 --- a/src/Pure/System/session.ML	Sun Nov 18 16:31:41 2012 +0100
     3.2 +++ b/src/Pure/System/session.ML	Sun Nov 18 19:01:30 2012 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4    val welcome: unit -> string
     3.5    val finish: unit -> unit
     3.6    val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     3.7 -    string -> string -> string * Present.dump_mode -> string -> bool -> unit
     3.8 +    string -> string -> bool * string -> string -> bool -> unit
     3.9    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    3.10    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    3.11      string -> bool -> string list -> string -> string -> bool * string ->
    3.12 @@ -115,8 +115,6 @@
    3.13  
    3.14  local
    3.15  
    3.16 -fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
    3.17 -
    3.18  fun read_variants strs =
    3.19    rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
    3.20    |> filter_out (fn (_, s) => s = "-");
    3.21 @@ -124,7 +122,7 @@
    3.22  in
    3.23  
    3.24  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    3.25 -    name dump rpath level timing verbose max_threads trace_threads
    3.26 +    name doc_dump rpath level timing verbose max_threads trace_threads
    3.27      parallel_proofs parallel_proofs_threshold =
    3.28    ((fn () =>
    3.29      let
    3.30 @@ -133,7 +131,7 @@
    3.31            "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
    3.32        val _ =
    3.33          init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
    3.34 -          (doc_dump dump) rpath verbose;
    3.35 +          doc_dump rpath verbose;
    3.36        val res1 = (use |> with_timing item timing |> Exn.capture) root;
    3.37        val res2 = Exn.capture finish ();
    3.38      in ignore (Par_Exn.release_all [res1, res2]) end)
     4.1 --- a/src/Pure/Thy/present.ML	Sun Nov 18 16:31:41 2012 +0100
     4.2 +++ b/src/Pure/Thy/present.ML	Sun Nov 18 19:01:30 2012 +0100
     4.3 @@ -13,11 +13,9 @@
     4.4  sig
     4.5    include BASIC_PRESENT
     4.6    val session_name: theory -> string
     4.7 -  datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
     4.8 -  val dump_mode: string -> dump_mode
     4.9    val read_variant: string -> string * string
    4.10    val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
    4.11 -    string list -> string -> string * dump_mode -> Url.T option * bool -> bool ->
    4.12 +    string list -> string -> bool * string -> Url.T option * bool -> bool ->
    4.13      theory list -> unit  (*not thread-safe!*)
    4.14    val finish: unit -> unit  (*not thread-safe!*)
    4.15    val init_theory: string -> unit
    4.16 @@ -190,18 +188,10 @@
    4.17  
    4.18  (* session_info *)
    4.19  
    4.20 -datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty;
    4.21 -
    4.22 -fun dump_mode "all" = Dump_all
    4.23 -  | dump_mode "tex" = Dump_tex
    4.24 -  | dump_mode "tex+sty" = Dump_tex_sty
    4.25 -  | dump_mode s =
    4.26 -      error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")");
    4.27 -
    4.28  type session_info =
    4.29    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    4.30      info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
    4.31 -    documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option,
    4.32 +    documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
    4.33      verbose: bool, readme: Path.T option};
    4.34  
    4.35  fun make_session_info
    4.36 @@ -261,7 +251,7 @@
    4.37  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    4.38  
    4.39  fun init build info info_path doc doc_graph document_output doc_variants path name
    4.40 -    (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
    4.41 +    (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys =
    4.42    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
    4.43      (browser_info := empty_browser_info; session_info := NONE)
    4.44    else
    4.45 @@ -348,7 +338,7 @@
    4.46  
    4.47  fun finish () =
    4.48    session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
    4.49 -    documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
    4.50 +    documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
    4.51    let
    4.52      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    4.53      val thys = Symtab.dest theories;
    4.54 @@ -383,14 +373,11 @@
    4.55          else ())
    4.56        else ();
    4.57  
    4.58 -    fun prepare_sources doc_dir doc_mode =
    4.59 +    fun prepare_sources doc_copy doc_dir =
    4.60       (Isabelle_System.mkdirs doc_dir;
    4.61 -      (case doc_mode of
    4.62 -        Dump_all => Isabelle_System.copy_dir document_path doc_dir
    4.63 -      | Dump_tex_sty =>
    4.64 -          ignore (Isabelle_System.isabelle_tool "latex"
    4.65 -            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    4.66 -      | Dump_tex => ());
    4.67 +      if doc_copy then Isabelle_System.copy_dir document_path doc_dir else ();
    4.68 +      Isabelle_System.isabelle_tool "latex"
    4.69 +        ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
    4.70        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    4.71          (File.write (Path.append doc_dir graph_pdf_path) pdf;
    4.72            File.write (Path.append doc_dir graph_eps_path) eps));
    4.73 @@ -402,7 +389,7 @@
    4.74        else
    4.75          let
    4.76            val path = Path.explode dump_prefix;
    4.77 -          val _ = prepare_sources path dump_mode;
    4.78 +          val _ = prepare_sources dump_copy path;
    4.79          in
    4.80            if verbose then
    4.81              Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
    4.82 @@ -415,8 +402,8 @@
    4.83            File.eq (document_path, doc_prefix) andalso
    4.84              error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    4.85          val dir = Path.append doc_prefix (Path.basic name);
    4.86 -        val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
    4.87 -        val _ = prepare_sources dir mode;
    4.88 +        val copy = not (File.eq (document_path, dir));
    4.89 +        val _ = prepare_sources copy dir;
    4.90          fun inform doc =
    4.91            if verbose orelse not backdrop then
    4.92              Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")