# HG changeset patch
# User haftmann
# Date 1393148023 -3600
# Node ID 1f89921f3e758d346c7c45ada65b27aedf926339
# Parent  fb46f1c379b549f96484454f7267e196941d14d8
dropped long-unused option

diff -r fb46f1c379b5 -r 1f89921f3e75 NEWS
--- a/NEWS	Sun Feb 23 10:33:43 2014 +0100
+++ b/NEWS	Sun Feb 23 10:33:43 2014 +0100
@@ -90,6 +90,8 @@
 
 *** HOL ***
 
+* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
+
 * Simproc "finite_Collect" is no longer enabled by default, due to
 spurious crashes and other surprises.  Potential INCOMPATIBILITY.
 
diff -r fb46f1c379b5 -r 1f89921f3e75 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
@@ -2535,10 +2535,7 @@
   module hierarchy.  Omitting the file specification denotes standard
   output.
 
-  Serializers take an optional list of arguments in parentheses.  For
-  \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
-  explicit module signatures.
-
+  Serializers take an optional list of arguments in parentheses.
   For \emph{Haskell} a module name prefix may be given using the
   ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
   ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
diff -r fb46f1c379b5 -r 1f89921f3e75 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
@@ -335,13 +335,13 @@
           end;
   in print_stmt end;
 
-fun print_sml_module name some_decls body =
+fun print_sml_module name decls body =
   Pretty.chunks2 (
-    Pretty.chunks (
-      str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
-      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
-      @| (if is_some some_decls then str "end = struct" else str "struct")
-    )
+    Pretty.chunks [
+      str ("structure " ^ name ^ " : sig"),
+      (indent 2 o Pretty.chunks) decls,
+      str "end = struct"
+    ]
     :: body
     @| str ("end; (*struct " ^ name ^ "*)")
   );
@@ -665,13 +665,13 @@
           end;
   in print_stmt end;
 
-fun print_ocaml_module name some_decls body =
+fun print_ocaml_module name decls body =
   Pretty.chunks2 (
-    Pretty.chunks (
-      str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
-      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
-      @| (if is_some some_decls then str "end = struct" else str "struct")
-    )
+    Pretty.chunks [
+      str ("module " ^ name ^ " : sig"),
+      (indent 2 o Pretty.chunks) decls,
+      str "end = struct"
+    ]
     :: body
     @| str ("end;; (*struct " ^ name ^ "*)")
   );
@@ -785,7 +785,7 @@
       cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
   end;
 
-fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
+fun serialize_ml print_ml_module print_ml_stmt ctxt
     { module_name, reserved_syms, identifiers, includes,
       class_syntax, tyco_syntax, const_syntax } program =
   let
@@ -804,7 +804,7 @@
     fun print_module _ base _ xs =
       let
         val (raw_decls, body) = split_list xs;
-        val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
+        val decls = maps these raw_decls
       in (NONE, print_ml_module base decls body) end;
 
     (* serialization *)
@@ -820,12 +820,10 @@
   end;
 
 val serializer_sml : Code_Target.serializer =
-  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
-  >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));
+  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
 
 val serializer_ocaml : Code_Target.serializer =
-  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
-  >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));
+  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
 
 
 (** Isar setup **)