# HG changeset patch
# User wenzelm
# Date 1343386879 -7200
# Node ID 93b558e05f21cf55b8f6832f68c31886a556a955
# Parent  0a5f598cacec9f42689277103c72d99d7c807dec
prefer explicit datatype Present.dump_mode;

diff -r 0a5f598cacec -r 93b558e05f21 src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Fri Jul 27 12:43:58 2012 +0200
+++ b/src/Pure/System/build.ML	Fri Jul 27 13:01:19 2012 +0200
@@ -71,7 +71,8 @@
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
         parent_name name
-        (Options.string options "document_dump", Options.string options "document_dump_mode")
+        (Options.string options "document_dump",
+          Present.dump_mode (Options.string options "document_dump_mode"))
         "" verbose;
     val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();
diff -r 0a5f598cacec -r 93b558e05f21 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Jul 27 12:43:58 2012 +0200
+++ b/src/Pure/System/session.ML	Fri Jul 27 13:01:19 2012 +0200
@@ -11,7 +11,7 @@
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
-    string -> string -> string * string -> string -> bool -> unit
+    string -> string -> string * Present.dump_mode -> 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 ->
@@ -112,7 +112,7 @@
 
 local
 
-fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty");
+fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
 
 in
 
diff -r 0a5f598cacec -r 93b558e05f21 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Jul 27 12:43:58 2012 +0200
+++ b/src/Pure/Thy/present.ML	Fri Jul 27 13:01:19 2012 +0200
@@ -17,8 +17,10 @@
    path: string, parents: string list} list -> Path.T -> unit
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
+  datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
+  val dump_mode: string -> dump_mode
   val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
-    string -> string * string -> Url.T option * bool -> bool ->
+    string -> string * dump_mode -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
@@ -207,10 +209,18 @@
 
 (* 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, documents: (string * string) list,
-    doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
+    doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
     readme: Path.T option};
 
 fun make_session_info
@@ -377,12 +387,12 @@
 
     fun prepare_sources doc_dir doc_mode =
      (Isabelle_System.mkdirs doc_dir;
-      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
-      else if doc_mode = "tex+sty" then
-        ignore (Isabelle_System.isabelle_tool "latex"
-          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
-      else if doc_mode = "tex" then ()
-      else error ("Illegal document dump mode: " ^ quote doc_mode);
+      (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 => ());
       (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));
@@ -424,7 +434,7 @@
       documents |> Par_List.map (fn (name, tags) =>
         let
           val path = Path.append html_prefix (Path.basic name);
-          val _ = prepare_sources path "all";
+          val _ = prepare_sources path Dump_all;
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =
       if verbose then