# HG changeset patch # User wenzelm # Date 1353261690 -3600 # Node ID 97d2b77313a08f1abc1c23d6cd16145597257e65 # Parent 245f5947233cd963b3bdaa1dddab5b933dfb19c3 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; diff -r 245f5947233c -r 97d2b77313a0 etc/options --- a/etc/options Sun Nov 18 16:31:41 2012 +0100 +++ b/etc/options Sun Nov 18 19:01:30 2012 +0100 @@ -13,10 +13,6 @@ -- "option alternative document variants (separated by colons)" option document_graph : bool = false -- "generate session graph image for document" -option document_dump : string = "" - -- "dump generated document sources into given directory" -option document_dump_mode : string = "all" - -- "specific document dump mode: all, tex, tex+sty" option show_question_marks : bool = true -- "show leading question mark of schematic variables" diff -r 245f5947233c -r 97d2b77313a0 src/Pure/System/build.ML --- a/src/Pure/System/build.ML Sun Nov 18 16:31:41 2012 +0100 +++ b/src/Pure/System/build.ML Sun Nov 18 19:01:30 2012 +0100 @@ -15,8 +15,7 @@ local fun no_document options = - (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso - (Options.string options "document_dump" = ""); + (case Options.string options "document" of "" => true | "false" => true | _ => false); fun use_thys options = Thy_Info.use_thys @@ -73,11 +72,6 @@ | dups => error ("Duplicate document variants: " ^ commas_quote dups)); val _ = - if Options.string options "document_dump" = "" then () - else - Output.physical_stderr - "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n"; - val _ = Session.init do_output false (Options.bool options "browser_info") browser_info (Options.string options "document") @@ -85,9 +79,8 @@ (Options.string options "document_output") document_variants parent_name name - (Options.string options "document_dump", - Present.dump_mode (Options.string options "document_dump_mode")) - "" verbose; + (false, "") "" + verbose; val res1 = theories |> diff -r 245f5947233c -r 97d2b77313a0 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Sun Nov 18 16:31:41 2012 +0100 +++ b/src/Pure/System/session.ML Sun Nov 18 19:01:30 2012 +0100 @@ -11,7 +11,7 @@ val welcome: unit -> string val finish: unit -> unit val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string -> string -> string * Present.dump_mode -> string -> bool -> unit + string -> string -> bool * string -> string -> bool -> unit val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> string -> bool -> string list -> string -> string -> bool * string -> @@ -115,8 +115,6 @@ local -fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty); - fun read_variants strs = rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs))) |> filter_out (fn (_, s) => s = "-"); @@ -124,7 +122,7 @@ in fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent - name dump rpath level timing verbose max_threads trace_threads + name doc_dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = ((fn () => let @@ -133,7 +131,7 @@ "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; val _ = init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name - (doc_dump dump) rpath verbose; + doc_dump rpath verbose; val res1 = (use |> with_timing item timing |> Exn.capture) root; val res2 = Exn.capture finish (); in ignore (Par_Exn.release_all [res1, res2]) end) diff -r 245f5947233c -r 97d2b77313a0 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Nov 18 16:31:41 2012 +0100 +++ b/src/Pure/Thy/present.ML Sun Nov 18 19:01:30 2012 +0100 @@ -13,11 +13,9 @@ sig include BASIC_PRESENT val session_name: theory -> string - datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty - val dump_mode: string -> dump_mode val read_variant: string -> string * string val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string list -> string -> string * dump_mode -> Url.T option * bool -> bool -> + string list -> string -> bool * string -> Url.T option * bool -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit @@ -190,18 +188,10 @@ (* session_info *) -datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty; - -fun dump_mode "all" = Dump_all - | dump_mode "tex" = Dump_tex - | dump_mode "tex+sty" = Dump_tex_sty - | dump_mode s = - error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")"); - type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, - documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option, + documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option, verbose: bool, readme: Path.T option}; fun make_session_info @@ -261,7 +251,7 @@ fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); fun init build info info_path doc doc_graph document_output doc_variants path name - (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys = + (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys = if not build andalso not info andalso doc = "" andalso dump_prefix = "" then (browser_info := empty_browser_info; session_info := NONE) else @@ -348,7 +338,7 @@ fun finish () = session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output, - documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} => + documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -383,14 +373,11 @@ else ()) else (); - fun prepare_sources doc_dir doc_mode = + fun prepare_sources doc_copy doc_dir = (Isabelle_System.mkdirs doc_dir; - (case doc_mode of - Dump_all => Isabelle_System.copy_dir document_path doc_dir - | Dump_tex_sty => - ignore (Isabelle_System.isabelle_tool "latex" - ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")))) - | Dump_tex => ()); + if doc_copy then Isabelle_System.copy_dir document_path doc_dir else (); + Isabelle_System.isabelle_tool "latex" + ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); (case opt_graphs of NONE => () | SOME (pdf, eps) => (File.write (Path.append doc_dir graph_pdf_path) pdf; File.write (Path.append doc_dir graph_eps_path) eps)); @@ -402,7 +389,7 @@ else let val path = Path.explode dump_prefix; - val _ = prepare_sources path dump_mode; + val _ = prepare_sources dump_copy path; in if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") @@ -415,8 +402,8 @@ File.eq (document_path, doc_prefix) andalso error ("Overlap of document input and output directory " ^ Path.print doc_prefix); val dir = Path.append doc_prefix (Path.basic name); - val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all; - val _ = prepare_sources dir mode; + val copy = not (File.eq (document_path, dir)); + val _ = prepare_sources copy dir; fun inform doc = if verbose orelse not backdrop then Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")