# HG changeset patch
# User wenzelm
# Date 1243247369 -7200
# Node ID dcbf876f55928a5209fb54304c8a2016110eda33
# Parent  2291e4d628eb8a5da7c0cfe27b525c57798f550a
adapted to Poly/ML SVN 744;

diff -r 2291e4d628eb -r dcbf876f5592 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Sat May 23 21:41:02 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Mon May 25 12:29:29 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 (SVN 719).
+Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
 *)
 
 signature ML_TEST =
@@ -44,11 +44,11 @@
 
 (* parse trees *)
 
-fun report_parse_tree context depth =
+fun report_parse_tree context depth space =
   let
     val pos_of = position_of (Context.proof_of context);
     fun report loc (PTtype types) =
-          PolyML.NameSpace.displayTypeExpression (types, depth)
+          PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
           |> Position.report_text Markup.ML_typing (pos_of loc)
       | report loc (PTdeclaredAt decl) =
@@ -132,7 +132,7 @@
 
     fun result_fun (phase1, phase2) () =
      (case phase1 of NONE => ()
-      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth parse_tree;
+      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
       case phase2 of NONE => error "Static Errors"
       | SOME code => apply_result (Toplevel.program code));