src/Pure/Thy/present.ML
changeset 48543 93b558e05f21
parent 48516 c5d0f19ef7cb
child 48804 6348e5fca42e
     1.1 --- a/src/Pure/Thy/present.ML	Fri Jul 27 12:43:58 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Fri Jul 27 13:01:19 2012 +0200
     1.3 @@ -17,8 +17,10 @@
     1.4     path: string, parents: string list} list -> Path.T -> unit
     1.5    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     1.6     path: string, parents: string list} list -> unit
     1.7 +  datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
     1.8 +  val dump_mode: string -> dump_mode
     1.9    val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
    1.10 -    string -> string * string -> Url.T option * bool -> bool ->
    1.11 +    string -> string * dump_mode -> Url.T option * bool -> bool ->
    1.12      theory list -> unit  (*not thread-safe!*)
    1.13    val finish: unit -> unit  (*not thread-safe!*)
    1.14    val init_theory: string -> unit
    1.15 @@ -207,10 +209,18 @@
    1.16  
    1.17  (* session_info *)
    1.18  
    1.19 +datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty;
    1.20 +
    1.21 +fun dump_mode "all" = Dump_all
    1.22 +  | dump_mode "tex" = Dump_tex
    1.23 +  | dump_mode "tex+sty" = Dump_tex_sty
    1.24 +  | dump_mode s =
    1.25 +      error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")");
    1.26 +
    1.27  type session_info =
    1.28    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    1.29      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
    1.30 -    doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
    1.31 +    doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
    1.32      readme: Path.T option};
    1.33  
    1.34  fun make_session_info
    1.35 @@ -377,12 +387,12 @@
    1.36  
    1.37      fun prepare_sources doc_dir doc_mode =
    1.38       (Isabelle_System.mkdirs doc_dir;
    1.39 -      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
    1.40 -      else if doc_mode = "tex+sty" then
    1.41 -        ignore (Isabelle_System.isabelle_tool "latex"
    1.42 -          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    1.43 -      else if doc_mode = "tex" then ()
    1.44 -      else error ("Illegal document dump mode: " ^ quote doc_mode);
    1.45 +      (case doc_mode of
    1.46 +        Dump_all => Isabelle_System.copy_dir document_path doc_dir
    1.47 +      | Dump_tex_sty =>
    1.48 +          ignore (Isabelle_System.isabelle_tool "latex"
    1.49 +            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    1.50 +      | Dump_tex => ());
    1.51        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.52          (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.53            File.write (Path.append doc_dir graph_eps_path) eps));
    1.54 @@ -424,7 +434,7 @@
    1.55        documents |> Par_List.map (fn (name, tags) =>
    1.56          let
    1.57            val path = Path.append html_prefix (Path.basic name);
    1.58 -          val _ = prepare_sources path "all";
    1.59 +          val _ = prepare_sources path Dump_all;
    1.60          in isabelle_document true doc_format name tags path html_prefix end);
    1.61      val _ =
    1.62        if verbose then