# 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 "" - | SOME (Exn.Exn _) => PrettyString "" + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" | 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 "" - | SOME (Exn.Exn _) => PrettyString "" + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" | 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;