equal
deleted
inserted
replaced
103 use "ML-Systems/compiler_polyml.ML"; |
103 use "ML-Systems/compiler_polyml.ML"; |
104 |
104 |
105 PolyML.Compiler.reportUnreferencedIds := true; |
105 PolyML.Compiler.reportUnreferencedIds := true; |
106 PolyML.Compiler.printInAlphabeticalOrder := false; |
106 PolyML.Compiler.printInAlphabeticalOrder := false; |
107 PolyML.Compiler.maxInlineSize := 80; |
107 PolyML.Compiler.maxInlineSize := 80; |
|
108 (*PolyML.Compiler.reportExhaustiveHandlers := true;*) |
108 |
109 |
109 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
110 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
110 |
111 |
111 |
112 |
112 (* ML toplevel pretty printing *) |
113 (* ML toplevel pretty printing *) |