# HG changeset patch
# User wenzelm
# Date 1243093159 -7200
# Node ID 67c796138bf077ddb71423fb894000666151d89c
# Parent  6ce6801129de3eb657a69075b06f65305aed0c71
adapted to Poly/ML SVN 719;
removed obsolete add_prefix;

diff -r 6ce6801129de -r 67c796138bf0 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Sat May 23 17:21:44 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Sat May 23 17:39:19 2009 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_test.ML
     Author:     Makarius
 
-Test of advanced ML compiler invocation in Poly/ML 5.3.
+Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 719).
 *)
 
 signature ML_TEST =
@@ -101,33 +101,18 @@
     (* results *)
 
     val depth = get_print_depth ();
-    val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
-        fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) =
-              let
-                fun make_prefix context =
-                  (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of
-                    SOME (name, sub_context) => make_prefix sub_context ^ name ^ "."
-                  | NONE => prefix);
-                val this_prefix = make_prefix context;
-              in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end
-          | add_prefix prefix (prt as PrettyString s) =
-              if prefix = "" then prt else PrettyString (prefix ^ s)
-          | add_prefix _ (prt as PrettyBreak _) = prt;
-
         fun display disp x =
           if depth > 0 then
-            (disp x
-              |> with_struct ? add_prefix ""
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
           else ();
 
         fun apply_fix (a, b) =
           (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
         fun apply_type (a, b) =
-          (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b));
+          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
         fun apply_sig (a, b) =
           (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
         fun apply_struct (a, b) =