src/Pure/ML-Systems/polyml.ML
changeset 4977 6cec2c0ffdbf
parent 4428 5c26253b8a2e
child 4984 d17004d4c13b
--- a/src/Pure/ML-Systems/polyml.ML	Thu May 28 11:11:27 1998 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu May 28 12:21:05 1998 +0200
@@ -27,6 +27,11 @@
   " secs";
 
 
+(* prompts *)
+
+fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt1 := p2);
+
+
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
 
 fun make_pp _ pprint (str, blk, brk, en) obj =