report ML typing;
authorwenzelm
Tue, 24 Mar 2009 18:21:58 +0100
changeset 30709d9ca766bf24c
parent 30708 83df88b6d082
child 30710 77d4b1284d4c
report ML typing;
src/Pure/ML/ml_test.ML
     1.1 --- a/src/Pure/ML/ml_test.ML	Tue Mar 24 16:11:42 2009 +0100
     1.2 +++ b/src/Pure/ML/ml_test.ML	Tue Mar 24 18:21:58 2009 +0100
     1.3 @@ -43,11 +43,13 @@
     1.4  
     1.5  (* parse trees *)
     1.6  
     1.7 -fun report_parse_tree context =
     1.8 +fun report_parse_tree context depth =
     1.9    let
    1.10      val pos_of = pos_of_location context;
    1.11 -    fun report loc (PTtype types) =  (* FIXME body text *)
    1.12 -          Position.report Markup.ML_typing (pos_of loc)
    1.13 +    fun report loc (PTtype types) =
    1.14 +          PolyML.NameSpace.displayTypeExpression (types, depth)
    1.15 +          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    1.16 +          |> Position.report_text Markup.ML_typing (pos_of loc)
    1.17        | report loc (PTdeclaredAt decl) =
    1.18            Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
    1.19            |> Position.report_text Markup.ML_ref (pos_of loc)
    1.20 @@ -96,6 +98,9 @@
    1.21  
    1.22      (* results *)
    1.23  
    1.24 +    val depth = get_print_depth ();
    1.25 +    val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
    1.26 +
    1.27      fun apply_result {fixes, types, signatures, structures, functors, values} =
    1.28        let
    1.29          fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) =
    1.30 @@ -110,9 +115,6 @@
    1.31                if prefix = "" then prt else PrettyString (prefix ^ s)
    1.32            | add_prefix _ (prt as PrettyBreak _) = prt;
    1.33  
    1.34 -        val depth = get_print_depth ();
    1.35 -        val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
    1.36 -
    1.37          fun display disp x =
    1.38            if depth > 0 then
    1.39              (disp x
    1.40 @@ -143,7 +145,7 @@
    1.41  
    1.42      fun result_fun (phase1, phase2) () =
    1.43       (case phase1 of NONE => ()
    1.44 -      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) parse_tree;
    1.45 +      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth parse_tree;
    1.46        case phase2 of NONE => error "Static Errors"
    1.47        | SOME code => apply_result (Toplevel.program code));
    1.48