src/Tools/Code/code_ml.ML
changeset 55677 1f89921f3e75
parent 55657 d5ad50aea356
child 55679 59244fc1a7ca
     1.1 --- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -335,13 +335,13 @@
     1.4            end;
     1.5    in print_stmt end;
     1.6  
     1.7 -fun print_sml_module name some_decls body =
     1.8 +fun print_sml_module name decls body =
     1.9    Pretty.chunks2 (
    1.10 -    Pretty.chunks (
    1.11 -      str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    1.12 -      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
    1.13 -      @| (if is_some some_decls then str "end = struct" else str "struct")
    1.14 -    )
    1.15 +    Pretty.chunks [
    1.16 +      str ("structure " ^ name ^ " : sig"),
    1.17 +      (indent 2 o Pretty.chunks) decls,
    1.18 +      str "end = struct"
    1.19 +    ]
    1.20      :: body
    1.21      @| str ("end; (*struct " ^ name ^ "*)")
    1.22    );
    1.23 @@ -665,13 +665,13 @@
    1.24            end;
    1.25    in print_stmt end;
    1.26  
    1.27 -fun print_ocaml_module name some_decls body =
    1.28 +fun print_ocaml_module name decls body =
    1.29    Pretty.chunks2 (
    1.30 -    Pretty.chunks (
    1.31 -      str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
    1.32 -      :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
    1.33 -      @| (if is_some some_decls then str "end = struct" else str "struct")
    1.34 -    )
    1.35 +    Pretty.chunks [
    1.36 +      str ("module " ^ name ^ " : sig"),
    1.37 +      (indent 2 o Pretty.chunks) decls,
    1.38 +      str "end = struct"
    1.39 +    ]
    1.40      :: body
    1.41      @| str ("end;; (*struct " ^ name ^ "*)")
    1.42    );
    1.43 @@ -785,7 +785,7 @@
    1.44        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    1.45    end;
    1.46  
    1.47 -fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
    1.48 +fun serialize_ml print_ml_module print_ml_stmt ctxt
    1.49      { module_name, reserved_syms, identifiers, includes,
    1.50        class_syntax, tyco_syntax, const_syntax } program =
    1.51    let
    1.52 @@ -804,7 +804,7 @@
    1.53      fun print_module _ base _ xs =
    1.54        let
    1.55          val (raw_decls, body) = split_list xs;
    1.56 -        val decls = if with_signatures then SOME (maps these raw_decls) else NONE 
    1.57 +        val decls = maps these raw_decls
    1.58        in (NONE, print_ml_module base decls body) end;
    1.59  
    1.60      (* serialization *)
    1.61 @@ -820,12 +820,10 @@
    1.62    end;
    1.63  
    1.64  val serializer_sml : Code_Target.serializer =
    1.65 -  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.66 -  >> (fn with_signatures => serialize_ml print_sml_module print_sml_stmt with_signatures));
    1.67 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_sml_module print_sml_stmt);
    1.68  
    1.69  val serializer_ocaml : Code_Target.serializer =
    1.70 -  Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    1.71 -  >> (fn with_signatures => serialize_ml print_ocaml_module print_ocaml_stmt with_signatures));
    1.72 +  Code_Target.parse_args (Scan.succeed ()) #> K (serialize_ml print_ocaml_module print_ocaml_stmt);
    1.73  
    1.74  
    1.75  (** Isar setup **)