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