ML results: enter before printing (cf. Poly/ML SVN 1218);
authorwenzelm
Sun, 28 Nov 2010 20:36:45 +0100
changeset 40799 d44c87988a24
parent 40798 0562a0a5bb93
child 40800 330eb65c9469
ML results: enter before printing (cf. Poly/ML SVN 1218);
src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Nov 28 20:12:22 2010 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Nov 28 20:36:45 2010 +0100
@@ -140,17 +140,17 @@
           else ();
 
         fun apply_fix (a, b) =
-          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
+          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
         fun apply_type (a, b) =
-          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
+          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
         fun apply_sig (a, b) =
-          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
+          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
         fun apply_struct (a, b) =
-          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
+          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
         fun apply_funct (a, b) =
-          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
+          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
         fun apply_val (a, b) =
-          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
+          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
       in
         List.app apply_fix fixes;
         List.app apply_type types;