prefer explicit datatype Present.dump_mode;
authorwenzelm
Fri Jul 27 13:01:19 2012 +0200 (2012-07-27)
changeset 4854393b558e05f21
parent 48542 0a5f598cacec
child 48544 8c26657e73c3
prefer explicit datatype Present.dump_mode;
src/Pure/System/build.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/System/build.ML	Fri Jul 27 12:43:58 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Fri Jul 27 13:01:19 2012 +0200
     1.3 @@ -71,7 +71,8 @@
     1.4          (Options.bool options "document_graph")
     1.5          (space_explode ":" (Options.string options "document_variants"))
     1.6          parent_name name
     1.7 -        (Options.string options "document_dump", Options.string options "document_dump_mode")
     1.8 +        (Options.string options "document_dump",
     1.9 +          Present.dump_mode (Options.string options "document_dump_mode"))
    1.10          "" verbose;
    1.11      val _ = Session.with_timing name timing (List.app use_theories) theories;
    1.12      val _ = Session.finish ();
     2.1 --- a/src/Pure/System/session.ML	Fri Jul 27 12:43:58 2012 +0200
     2.2 +++ b/src/Pure/System/session.ML	Fri Jul 27 13:01:19 2012 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4    val welcome: unit -> string
     2.5    val finish: unit -> unit
     2.6    val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
     2.7 -    string -> string -> string * string -> string -> bool -> unit
     2.8 +    string -> string -> string * Present.dump_mode -> string -> bool -> unit
     2.9    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    2.10    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    2.11      string -> bool -> string list -> string -> string -> bool * string ->
    2.12 @@ -112,7 +112,7 @@
    2.13  
    2.14  local
    2.15  
    2.16 -fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty");
    2.17 +fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
    2.18  
    2.19  in
    2.20  
     3.1 --- a/src/Pure/Thy/present.ML	Fri Jul 27 12:43:58 2012 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Fri Jul 27 13:01:19 2012 +0200
     3.3 @@ -17,8 +17,10 @@
     3.4     path: string, parents: string list} list -> Path.T -> unit
     3.5    val display_graph: {name: string, ID: string, dir: string, unfold: bool,
     3.6     path: string, parents: string list} list -> unit
     3.7 +  datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
     3.8 +  val dump_mode: string -> dump_mode
     3.9    val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
    3.10 -    string -> string * string -> Url.T option * bool -> bool ->
    3.11 +    string -> string * dump_mode -> Url.T option * bool -> bool ->
    3.12      theory list -> unit  (*not thread-safe!*)
    3.13    val finish: unit -> unit  (*not thread-safe!*)
    3.14    val init_theory: string -> unit
    3.15 @@ -207,10 +209,18 @@
    3.16  
    3.17  (* session_info *)
    3.18  
    3.19 +datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty;
    3.20 +
    3.21 +fun dump_mode "all" = Dump_all
    3.22 +  | dump_mode "tex" = Dump_tex
    3.23 +  | dump_mode "tex+sty" = Dump_tex_sty
    3.24 +  | dump_mode s =
    3.25 +      error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")");
    3.26 +
    3.27  type session_info =
    3.28    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    3.29      info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
    3.30 -    doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
    3.31 +    doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
    3.32      readme: Path.T option};
    3.33  
    3.34  fun make_session_info
    3.35 @@ -377,12 +387,12 @@
    3.36  
    3.37      fun prepare_sources doc_dir doc_mode =
    3.38       (Isabelle_System.mkdirs doc_dir;
    3.39 -      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
    3.40 -      else if doc_mode = "tex+sty" then
    3.41 -        ignore (Isabelle_System.isabelle_tool "latex"
    3.42 -          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    3.43 -      else if doc_mode = "tex" then ()
    3.44 -      else error ("Illegal document dump mode: " ^ quote doc_mode);
    3.45 +      (case doc_mode of
    3.46 +        Dump_all => Isabelle_System.copy_dir document_path doc_dir
    3.47 +      | Dump_tex_sty =>
    3.48 +          ignore (Isabelle_System.isabelle_tool "latex"
    3.49 +            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    3.50 +      | Dump_tex => ());
    3.51        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    3.52          (File.write (Path.append doc_dir graph_pdf_path) pdf;
    3.53            File.write (Path.append doc_dir graph_eps_path) eps));
    3.54 @@ -424,7 +434,7 @@
    3.55        documents |> Par_List.map (fn (name, tags) =>
    3.56          let
    3.57            val path = Path.append html_prefix (Path.basic name);
    3.58 -          val _ = prepare_sources path "all";
    3.59 +          val _ = prepare_sources path Dump_all;
    3.60          in isabelle_document true doc_format name tags path html_prefix end);
    3.61      val _ =
    3.62        if verbose then