--- a/src/Tools/Code/code_scala.ML Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 02 14:36:49 2010 +0200
@@ -368,21 +368,15 @@
in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
fun print_node _ (_, Code_Namespace.Dummy) = NONE
| print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
- if null presentation_names
- orelse member (op =) presentation_names name
- then SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
- else NONE
+ SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
| print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
- if null presentation_names
- then
- let
- val prefix_fragments' = prefix_fragments @ [name_fragment];
- in
- Option.map (print_module name_fragment
- (map_filter (print_implicit prefix_fragments') implicits))
- (print_nodes prefix_fragments' nodes)
- end
- else print_nodes [] nodes
+ let
+ val prefix_fragments' = prefix_fragments @ [name_fragment];
+ in
+ Option.map (print_module name_fragment
+ (map_filter (print_implicit prefix_fragments') implicits))
+ (print_nodes prefix_fragments' nodes)
+ end
and print_nodes prefix_fragments nodes = let
val ps = map_filter (fn name => print_node prefix_fragments (name,
snd (Graph.get_node nodes name)))
@@ -390,8 +384,7 @@
in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
(* serialization *)
- val p_includes = if null presentation_names then map snd includes else [];
- val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
+ val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
in