# HG changeset patch
# User wenzelm
# Date 1243780179 -7200
# Node ID 133d1cfd6ae70cd6d0efb219d5a69623a9e0058d
# Parent  1f5740424c69e7a84bc9568b89e409999ab7aaf1
explicit PolyML qualification;

diff -r 1f5740424c69 -r 133d1cfd6ae7 src/Pure/ML-Systems/install_pp_polyml-experimental.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Sun May 31 15:49:35 2009 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Sun May 31 16:29:39 2009 +0200
@@ -3,15 +3,15 @@
 Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
 *)
 
-addPrettyPrinter (fn depth => fn pretty => fn x =>
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Future.peek x of
-    NONE => PrettyString "<future>"
-  | SOME (Exn.Exn _) => PrettyString "<failed>"
+    NONE => PolyML.PrettyString "<future>"
+  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   | SOME (Exn.Result y) => pretty (y, depth)));
 
-addPrettyPrinter (fn depth => fn pretty => fn x =>
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
-    NONE => PrettyString "<lazy>"
-  | SOME (Exn.Exn _) => PrettyString "<failed>"
+    NONE => PolyML.PrettyString "<lazy>"
+  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   | SOME (Exn.Result y) => pretty (y, depth)));
 
diff -r 1f5740424c69 -r 133d1cfd6ae7 src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Sun May 31 15:49:35 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sun May 31 16:29:39 2009 +0200
@@ -26,34 +26,35 @@
 
 val pretty_ml =
   let
-    fun convert len (PrettyBlock (ind, _, context, prts)) =
+    fun convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
           let
             fun property name default =
-              (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (ContextProperty (_, b)) => b
+              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+                SOME (PolyML.ContextProperty (_, b)) => b
               | NONE => default);
             val bg = property "begin" "";
             val en = property "end" "";
             val len' = property "length" len;
           in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
-      | convert len (PrettyString s) =
+      | convert len (PolyML.PrettyString s) =
           ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
-      | convert _ (PrettyBreak (wd, _)) =
+      | convert _ (PolyML.PrettyBreak (wd, _)) =
           ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
   in convert "" end;
 
 fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
       let val context =
-        (if bg = "" then [] else [ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [ContextProperty ("end", en)])
-      in PrettyBlock (ind, false, context, map ml_pretty prts) end
+        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+      in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
   | ml_pretty (ML_Pretty.String (s, len)) =
-      if len = size s then PrettyString s
-      else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
-  | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
-  | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+      if len = size s then PolyML.PrettyString s
+      else PolyML.PrettyBlock
+        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s])
+  | ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
+  | ml_pretty (ML_Pretty.Break (true, _)) = PolyML.PrettyBreak (99999, 0);
 
 fun toplevel_pp context (_: string list) pp =
   use_text context (1, "pp") false
-    ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 1f5740424c69 -r 133d1cfd6ae7 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Sun May 31 15:49:35 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Sun May 31 16:29:39 2009 +0200
@@ -35,7 +35,7 @@
   in (regs, context') end;
 
 fun position_of ctxt
-    ({file, startLine = line, startPosition = i, endPosition = j, ...}: location) =
+    ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
   (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
     (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
   | (SOME pos, NONE) => pos
@@ -47,15 +47,15 @@
 fun report_parse_tree context depth space =
   let
     val pos_of = position_of (Context.proof_of context);
-    fun report loc (PTtype types) =
+    fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
           |> Position.report_text Markup.ML_typing (pos_of loc)
-      | report loc (PTdeclaredAt decl) =
+      | report loc (PolyML.PTdeclaredAt decl) =
           Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
           |> Position.report_text Markup.ML_ref (pos_of loc)
-      | report _ (PTnextSibling tree) = report_tree (tree ())
-      | report _ (PTfirstChild tree) = report_tree (tree ())
+      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
+      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
       | report _ _ = ()
     and report_tree (loc, props) = List.app (report loc) props;
   in report_tree end;