src/Tools/Code/code_ml.ML
changeset 39057 c6d146ed07ae
parent 39056 fa197571676b
child 39058 551fe1af03b0
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 13:58:16 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 14:36:49 2010 +0200
     1.3 @@ -790,7 +790,6 @@
     1.4    const_syntax, program, names, presentation_names } =
     1.5    let
     1.6      val is_cons = Code_Thingol.is_cons program;
     1.7 -    val is_presentation = not (null presentation_names);
     1.8      val { deresolver, hierarchical_program = ml_program } =
     1.9        ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    1.10      val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
    1.11 @@ -798,15 +797,11 @@
    1.12      fun print_node _ (_, Code_Namespace.Dummy) =
    1.13            NONE
    1.14        | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    1.15 -          if is_presentation andalso
    1.16 -            (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
    1.17 -          then NONE
    1.18 -          else SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    1.19 +          SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    1.20        | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
    1.21            let
    1.22              val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
    1.23 -            val p = if is_presentation then Pretty.chunks2 body
    1.24 -              else print_module name_fragment
    1.25 +            val p = print_module name_fragment
    1.26                  (if with_signatures then SOME decls else NONE) body;
    1.27            in SOME ([], p) end
    1.28      and print_nodes prefix_fragments nodes = (map_filter