dropped long-unused option
authorhaftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 556771f89921f3e75
parent 55676 fb46f1c379b5
child 55678 aec339197a40
dropped long-unused option
NEWS
src/Doc/IsarRef/HOL_Specific.thy
src/Tools/Code/code_ml.ML
     1.1 --- a/NEWS	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/NEWS	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -90,6 +90,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
     1.8 +
     1.9  * Simproc "finite_Collect" is no longer enabled by default, due to
    1.10  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
    1.11  
     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
     2.3 @@ -2535,10 +2535,7 @@
     2.4    module hierarchy.  Omitting the file specification denotes standard
     2.5    output.
     2.6  
     2.7 -  Serializers take an optional list of arguments in parentheses.  For
     2.8 -  \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
     2.9 -  explicit module signatures.
    2.10 -
    2.11 +  Serializers take an optional list of arguments in parentheses.
    2.12    For \emph{Haskell} a module name prefix may be given using the
    2.13    ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
    2.14    ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
     3.1 --- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     3.2 +++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     3.3 @@ -335,13 +335,13 @@
     3.4            end;
     3.5    in print_stmt end;
     3.6  
     3.7 -fun print_sml_module name some_decls body =
     3.8 +fun print_sml_module name decls body =
     3.9    Pretty.chunks2 (
    3.10 -    Pretty.chunks (
    3.11 -      str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    3.12 -      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
    3.13 -      @| (if is_some some_decls then str "end = struct" else str "struct")
    3.14 -    )
    3.15 +    Pretty.chunks [
    3.16 +      str ("structure " ^ name ^ " : sig"),
    3.17 +      (indent 2 o Pretty.chunks) decls,
    3.18 +      str "end = struct"
    3.19 +    ]
    3.20      :: body
    3.21      @| str ("end; (*struct " ^ name ^ "*)")
    3.22    );
    3.23 @@ -665,13 +665,13 @@
    3.24            end;
    3.25    in print_stmt end;
    3.26  
    3.27 -fun print_ocaml_module name some_decls body =
    3.28 +fun print_ocaml_module name decls body =
    3.29    Pretty.chunks2 (
    3.30 -    Pretty.chunks (
    3.31 -      str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    3.32 -      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
    3.33 -      @| (if is_some some_decls then str "end = struct" else str "struct")
    3.34 -    )
    3.35 +    Pretty.chunks [
    3.36 +      str ("module " ^ name ^ " : sig"),
    3.37 +      (indent 2 o Pretty.chunks) decls,
    3.38 +      str "end = struct"
    3.39 +    ]
    3.40      :: body
    3.41      @| str ("end;; (*struct " ^ name ^ "*)")
    3.42    );
    3.43 @@ -785,7 +785,7 @@
    3.44        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    3.45    end;
    3.46  
    3.47 -fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
    3.48 +fun serialize_ml print_ml_module print_ml_stmt ctxt
    3.49      { module_name, reserved_syms, identifiers, includes,
    3.50        class_syntax, tyco_syntax, const_syntax } program =
    3.51    let
    3.52 @@ -804,7 +804,7 @@
    3.53      fun print_module _ base _ xs =
    3.54        let
    3.55          val (raw_decls, body) = split_list xs;
    3.56 -        val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
    3.57 +        val decls = maps these raw_decls
    3.58        in (NONE, print_ml_module base decls body) end;
    3.59  
    3.60      (* serialization *)
    3.61 @@ -820,12 +820,10 @@
    3.62    end;
    3.63  
    3.64  val serializer_sml : Code_Target.serializer =
    3.65 -  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    3.66 -  >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));
    3.67 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
    3.68  
    3.69  val serializer_ocaml : Code_Target.serializer =
    3.70 -  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    3.71 -  >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));
    3.72 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
    3.73  
    3.74  
    3.75  (** Isar setup **)