# HG changeset patch
# User wenzelm
# Date 896350865 -7200
# Node ID 6cec2c0ffdbf4f52ef334dbb16802a8dfe7db86b
# Parent  19f48dafe5d3aaf906637b3c9f587c4653f3bca5
added ml_prompts;

diff -r 19f48dafe5d3 -r 6cec2c0ffdbf src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Thu May 28 11:11:27 1998 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Thu May 28 12:21:05 1998 +0200
@@ -38,6 +38,10 @@
 fun make_pp path pprint = ();
 fun install_pp _ = ();
 
+(*prompts*)
+(*n.a.??*)
+fun ml_prompts p1 p2 = ();
+
 
 (** Compiler-independent timing functions **)
 
diff -r 19f48dafe5d3 -r 6cec2c0ffdbf src/Pure/ML-Systems/polyml.ML
--- 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 =
diff -r 19f48dafe5d3 -r 6cec2c0ffdbf src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu May 28 11:11:27 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu May 28 12:21:05 1998 +0200
@@ -56,6 +56,9 @@
 end;
 
 
+(* prompts *)
+
+fun ml_prompts p1 p2 = ();
 
 
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
diff -r 19f48dafe5d3 -r 6cec2c0ffdbf src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu May 28 11:11:27 1998 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu May 28 12:21:05 1998 +0200
@@ -34,9 +34,6 @@
  (Compiler.Control.Print.printDepth := n div 2;
   Compiler.Control.Print.printLength := n);
 
-(*Poly/ML-like prompts*)
-Compiler.Control.primaryPrompt := "> ";
-Compiler.Control.secondaryPrompt := "# ";
 
 
 (** Compiler-independent timing functions **)
@@ -59,6 +56,12 @@
   end;
 
 
+(* prompts *)
+
+fun ml_prompts p1 p2 =
+  (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
+
+
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
 
 fun make_pp path pprint =