equal
deleted
inserted
replaced
116 use "ML-Systems/compiler_polyml.ML"; |
116 use "ML-Systems/compiler_polyml.ML"; |
117 |
117 |
118 PolyML.Compiler.reportUnreferencedIds := true; |
118 PolyML.Compiler.reportUnreferencedIds := true; |
119 PolyML.Compiler.printInAlphabeticalOrder := false; |
119 PolyML.Compiler.printInAlphabeticalOrder := false; |
120 PolyML.Compiler.maxInlineSize := 80; |
120 PolyML.Compiler.maxInlineSize := 80; |
121 (*PolyML.Compiler.reportExhaustiveHandlers := true;*) |
|
122 |
121 |
123 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
122 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
124 |
123 |
125 |
124 |
126 (* ML toplevel pretty printing *) |
125 (* ML toplevel pretty printing *) |