99 |
99 |
100 |
100 |
101 (* results *) |
101 (* results *) |
102 |
102 |
103 val depth = get_print_depth (); |
103 val depth = get_print_depth (); |
104 val with_struct = ! PolyML.Compiler.printTypesWithStructureName; |
|
105 |
104 |
106 fun apply_result {fixes, types, signatures, structures, functors, values} = |
105 fun apply_result {fixes, types, signatures, structures, functors, values} = |
107 let |
106 let |
108 fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) = |
|
109 let |
|
110 fun make_prefix context = |
|
111 (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of |
|
112 SOME (name, sub_context) => make_prefix sub_context ^ name ^ "." |
|
113 | NONE => prefix); |
|
114 val this_prefix = make_prefix context; |
|
115 in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end |
|
116 | add_prefix prefix (prt as PrettyString s) = |
|
117 if prefix = "" then prt else PrettyString (prefix ^ s) |
|
118 | add_prefix _ (prt as PrettyBreak _) = prt; |
|
119 |
|
120 fun display disp x = |
107 fun display disp x = |
121 if depth > 0 then |
108 if depth > 0 then |
122 (disp x |
109 (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") |
123 |> with_struct ? add_prefix "" |
|
124 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n") |
|
125 else (); |
110 else (); |
126 |
111 |
127 fun apply_fix (a, b) = |
112 fun apply_fix (a, b) = |
128 (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); |
113 (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b)); |
129 fun apply_type (a, b) = |
114 fun apply_type (a, b) = |
130 (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b)); |
115 (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b)); |
131 fun apply_sig (a, b) = |
116 fun apply_sig (a, b) = |
132 (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); |
117 (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b)); |
133 fun apply_struct (a, b) = |
118 fun apply_struct (a, b) = |
134 (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); |
119 (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b)); |
135 fun apply_funct (a, b) = |
120 fun apply_funct (a, b) = |