clarified modules;
authorwenzelm
Fri Mar 18 16:26:35 2016 +0100 (2016-03-18 ago)
changeset 62663bea354f6ff21
parent 62662 291cc01f56f5
child 62664 083c9865c554
clarified modules;
tuned signature;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/binding.ML
src/Pure/General/path.ML
src/Pure/General/pretty.ML
src/Pure/General/sha1.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/install_pp_polyml.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ML/ml_syntax.ML
src/Pure/PIDE/xml.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Tools/debugger.ML
src/Pure/context.ML
src/Pure/morphism.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Mar 17 16:56:44 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Mar 18 16:26:35 2016 +0100
     1.3 @@ -99,6 +99,13 @@
     1.4  fun peek x = Single_Assignment.peek (result_of x);
     1.5  fun is_finished x = is_some (peek x);
     1.6  
     1.7 +val _ =
     1.8 +  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
     1.9 +    (case peek x of
    1.10 +      NONE => PolyML.PrettyString "<future>"
    1.11 +    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    1.12 +    | SOME (Exn.Res y) => pretty (y, depth)));
    1.13 +
    1.14  
    1.15  
    1.16  (** scheduling **)
    1.17 @@ -665,4 +672,3 @@
    1.18  end;
    1.19  
    1.20  type 'a future = 'a Future.future;
    1.21 -
     2.1 --- a/src/Pure/Concurrent/lazy.ML	Thu Mar 17 16:56:44 2016 +0100
     2.2 +++ b/src/Pure/Concurrent/lazy.ML	Fri Mar 18 16:26:35 2016 +0100
     2.3 @@ -99,7 +99,16 @@
     2.4    if is_finished x then Future.value_result (force_result x)
     2.5    else (singleton o Future.forks) params (fn () => force x);
     2.6  
     2.7 +
     2.8 +(* toplevel pretty printing *)
     2.9 +
    2.10 +val _ =
    2.11 +  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    2.12 +    (case peek x of
    2.13 +      NONE => PolyML.PrettyString "<lazy>"
    2.14 +    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    2.15 +    | SOME (Exn.Res y) => pretty (y, depth)));
    2.16 +
    2.17  end;
    2.18  
    2.19  type 'a lazy = 'a Lazy.lazy;
    2.20 -
     3.1 --- a/src/Pure/Concurrent/synchronized.ML	Thu Mar 17 16:56:44 2016 +0100
     3.2 +++ b/src/Pure/Concurrent/synchronized.ML	Fri Mar 18 16:26:35 2016 +0100
     3.3 @@ -66,4 +66,9 @@
     3.4  
     3.5  end;
     3.6  
     3.7 +
     3.8 +(* toplevel pretty printing *)
     3.9 +
    3.10 +val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth));
    3.11 +
    3.12  end;
     4.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Mar 17 16:56:44 2016 +0100
     4.2 +++ b/src/Pure/Concurrent/task_queue.ML	Fri Mar 18 16:26:35 2016 +0100
     4.3 @@ -394,4 +394,10 @@
     4.4          | NONE => ((NONE, deps'), queue)))
     4.5    end;
     4.6  
     4.7 +
     4.8 +(* toplevel pretty printing *)
     4.9 +
    4.10 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
    4.11 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
    4.12 +
    4.13  end;
     5.1 --- a/src/Pure/General/binding.ML	Thu Mar 17 16:56:44 2016 +0100
     5.2 +++ b/src/Pure/General/binding.ML	Fri Mar 18 16:26:35 2016 +0100
     5.3 @@ -35,7 +35,6 @@
     5.4    val concealed: binding -> binding
     5.5    val pretty: binding -> Pretty.T
     5.6    val print: binding -> string
     5.7 -  val pp: binding -> Pretty.T
     5.8    val bad: binding -> string
     5.9    val check: binding -> unit
    5.10    val name_spec: scope list -> (string * bool) list -> binding ->
    5.11 @@ -155,7 +154,7 @@
    5.12  
    5.13  val print = Pretty.unformatted_string_of o pretty;
    5.14  
    5.15 -val pp = pretty o set_pos Position.none;
    5.16 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
    5.17  
    5.18  
    5.19  (* check *)
    5.20 @@ -191,6 +190,7 @@
    5.21        andalso error (bad binding);
    5.22    in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
    5.23  
    5.24 +
    5.25  end;
    5.26  
    5.27  type binding = Binding.binding;
     6.1 --- a/src/Pure/General/path.ML	Thu Mar 17 16:56:44 2016 +0100
     6.2 +++ b/src/Pure/General/path.ML	Fri Mar 18 16:26:35 2016 +0100
     6.3 @@ -173,6 +173,8 @@
     6.4  
     6.5  val print = Pretty.unformatted_string_of o pretty;
     6.6  
     6.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
     6.8 +
     6.9  
    6.10  (* base element *)
    6.11  
     7.1 --- a/src/Pure/General/pretty.ML	Thu Mar 17 16:56:44 2016 +0100
     7.2 +++ b/src/Pure/General/pretty.ML	Fri Mar 18 16:26:35 2016 +0100
     7.3 @@ -74,6 +74,8 @@
     7.4    val writeln_chunks2: T list -> unit
     7.5    val to_ML: T -> ML_Pretty.pretty
     7.6    val from_ML: ML_Pretty.pretty -> T
     7.7 +  val to_polyml: T -> PolyML.pretty
     7.8 +  val from_polyml: PolyML.pretty -> T
     7.9  end;
    7.10  
    7.11  structure Pretty: PRETTY =
    7.12 @@ -372,7 +374,7 @@
    7.13  
    7.14  
    7.15  
    7.16 -(** ML toplevel pretty printing **)
    7.17 +(** toplevel pretty printing **)
    7.18  
    7.19  fun to_ML (Block (m, consistent, indent, prts, _)) =
    7.20        ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
    7.21 @@ -386,6 +388,12 @@
    7.22        Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
    7.23    | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
    7.24  
    7.25 +val to_polyml = to_ML #> ML_Pretty.to_polyml;
    7.26 +val from_polyml = ML_Pretty.from_polyml #> from_ML;
    7.27 +
    7.28  end;
    7.29  
    7.30 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn _: T => to_polyml (str "<pretty>"));
    7.31 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
    7.32 +
    7.33  end;
     8.1 --- a/src/Pure/General/sha1.ML	Thu Mar 17 16:56:44 2016 +0100
     8.2 +++ b/src/Pure/General/sha1.ML	Fri Mar 18 16:26:35 2016 +0100
     8.3 @@ -139,4 +139,6 @@
     8.4  
     8.5  val fake = Digest;
     8.6  
     8.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
     8.8 +
     8.9  end;
     9.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 17 16:56:44 2016 +0100
     9.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 18 16:26:35 2016 +0100
     9.3 @@ -173,6 +173,10 @@
     9.4        (context * thm list list -> state -> state) *
     9.5        (context * thm list list -> context -> context)};
     9.6  
     9.7 +val _ =
     9.8 +  PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
     9.9 +    Pretty.to_polyml (Pretty.str "<Proof.state>"));
    9.10 +
    9.11  fun make_goal (statement, using, goal, before_qed, after_qed) =
    9.12    Goal {statement = statement, using = using, goal = goal,
    9.13      before_qed = before_qed, after_qed = after_qed};
    10.1 --- a/src/Pure/Isar/toplevel.ML	Thu Mar 17 16:56:44 2016 +0100
    10.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 18 16:26:35 2016 +0100
    10.3 @@ -199,6 +199,8 @@
    10.4  
    10.5  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    10.6  
    10.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
    10.8 +
    10.9  
   10.10  
   10.11  (** toplevel transitions **)
    11.1 --- a/src/Pure/ML/install_pp_polyml.ML	Thu Mar 17 16:56:44 2016 +0100
    11.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Fri Mar 18 16:26:35 2016 +0100
    11.3 @@ -4,80 +4,20 @@
    11.4  ML toplevel pretty-printing for Poly/ML.
    11.5  *)
    11.6  
    11.7 -PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
    11.8 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
    11.9 -
   11.10 -PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
   11.11 -  ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
   11.12 -
   11.13 -PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
   11.14 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
   11.15 -
   11.16 -PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
   11.17 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
   11.18 -
   11.19 -PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
   11.20 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
   11.21 -
   11.22 -PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
   11.23 -  ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
   11.24 +PolyML.addPrettyPrinter
   11.25 +  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
   11.26  
   11.27 -PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
   11.28 -  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
   11.29 -
   11.30 -PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
   11.31 -  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
   11.32 -
   11.33 -PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
   11.34 -  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
   11.35 -
   11.36 -PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
   11.37 -  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
   11.38 -
   11.39 -PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
   11.40 -  ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
   11.41 -
   11.42 -PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
   11.43 -  ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
   11.44 +PolyML.addPrettyPrinter
   11.45 +  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
   11.46  
   11.47 -PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
   11.48 -  ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
   11.49 -
   11.50 -PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
   11.51 -  ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
   11.52 -
   11.53 -PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
   11.54 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
   11.55 -
   11.56 -PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
   11.57 -  ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
   11.58 -
   11.59 -PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
   11.60 -  ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
   11.61 -
   11.62 -PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
   11.63 -  ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
   11.64 +PolyML.addPrettyPrinter
   11.65 +  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
   11.66  
   11.67 -PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   11.68 -  ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
   11.69 -
   11.70 -PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
   11.71 -  ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
   11.72 -
   11.73 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   11.74 -  pretty (Synchronized.value var, depth));
   11.75 +PolyML.addPrettyPrinter
   11.76 +  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
   11.77  
   11.78 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   11.79 -  (case Future.peek x of
   11.80 -    NONE => PolyML.PrettyString "<future>"
   11.81 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   11.82 -  | SOME (Exn.Res y) => pretty (y, depth)));
   11.83 -
   11.84 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   11.85 -  (case Lazy.peek x of
   11.86 -    NONE => PolyML.PrettyString "<lazy>"
   11.87 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   11.88 -  | SOME (Exn.Res y) => pretty (y, depth)));
   11.89 +PolyML.addPrettyPrinter
   11.90 +  (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
   11.91  
   11.92  
   11.93  local
    12.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Mar 17 16:56:44 2016 +0100
    12.2 +++ b/src/Pure/ML/ml_compiler.ML	Fri Mar 18 16:26:35 2016 +0100
    12.3 @@ -65,7 +65,7 @@
    12.4            let
    12.5              val xml =
    12.6                ML_Name_Space.displayTypeExpression (types, depth, space)
    12.7 -              |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
    12.8 +              |> Pretty.from_polyml |> Pretty.string_of
    12.9                |> Output.output |> YXML.parse_body;
   12.10            in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
   12.11        end;
   12.12 @@ -193,7 +193,7 @@
   12.13          val pos = Exn_Properties.position_of_location loc;
   12.14          val txt =
   12.15            (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   12.16 -          Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
   12.17 +          Pretty.string_of (Pretty.from_polyml msg);
   12.18        in if hard then err txt else warn txt end;
   12.19  
   12.20  
   12.21 @@ -205,8 +205,7 @@
   12.22        let
   12.23          fun display disp x =
   12.24            if depth > 0 then
   12.25 -            (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
   12.26 -              write "\n")
   12.27 +            (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
   12.28            else ();
   12.29  
   12.30          fun apply_fix (a, b) =
    13.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 16:56:44 2016 +0100
    13.2 +++ b/src/Pure/ML/ml_pretty.ML	Fri Mar 18 16:26:35 2016 +0100
    13.3 @@ -114,8 +114,7 @@
    13.4  (* make string *)
    13.5  
    13.6  local
    13.7 -  fun pretty_string_of s =
    13.8 -    "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))";
    13.9 +  fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
   13.10    fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
   13.11  in
   13.12  
    14.1 --- a/src/Pure/ML/ml_syntax.ML	Thu Mar 17 16:56:44 2016 +0100
    14.2 +++ b/src/Pure/ML/ml_syntax.ML	Fri Mar 18 16:26:35 2016 +0100
    14.3 @@ -123,4 +123,8 @@
    14.4        else take (Int.max (max_len, 0)) body @ ["..."];
    14.5    in Pretty.str (quote (implode (map print_char body'))) end;
    14.6  
    14.7 +val _ =
    14.8 +  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
    14.9 +    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
   14.10 +
   14.11  end;
    15.1 --- a/src/Pure/PIDE/xml.ML	Thu Mar 17 16:56:44 2016 +0100
    15.2 +++ b/src/Pure/PIDE/xml.ML	Fri Mar 18 16:26:35 2016 +0100
    15.3 @@ -170,6 +170,9 @@
    15.4  fun pretty depth tree =
    15.5    Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
    15.6  
    15.7 +val _ =
    15.8 +  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
    15.9 +
   15.10  
   15.11  
   15.12  (** XML parsing **)
    16.1 --- a/src/Pure/Syntax/ast.ML	Thu Mar 17 16:56:44 2016 +0100
    16.2 +++ b/src/Pure/Syntax/ast.ML	Fri Mar 18 16:26:35 2016 +0100
    16.3 @@ -66,6 +66,8 @@
    16.4  fun pretty_rule (lhs, rhs) =
    16.5    Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
    16.6  
    16.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
    16.8 +
    16.9  
   16.10  (* strip_positions *)
   16.11  
    17.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Mar 17 16:56:44 2016 +0100
    17.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Mar 18 16:26:35 2016 +0100
    17.3 @@ -66,7 +66,6 @@
    17.4    val is_marked: string -> bool
    17.5    val dummy_type: term
    17.6    val fun_type: term
    17.7 -  val pp_lexicon: Scan.lexicon -> Pretty.T
    17.8  end;
    17.9  
   17.10  structure Lexicon: LEXICON =
   17.11 @@ -455,7 +454,8 @@
   17.12  
   17.13  (* toplevel pretty printing *)
   17.14  
   17.15 -val pp_lexicon =
   17.16 -  Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
   17.17 +val _ =
   17.18 +  PolyML.addPrettyPrinter (fn _ => fn _ =>
   17.19 +    Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
   17.20  
   17.21  end;
    18.1 --- a/src/Pure/Tools/debugger.ML	Thu Mar 17 16:56:44 2016 +0100
    18.2 +++ b/src/Pure/Tools/debugger.ML	Fri Mar 18 16:26:35 2016 +0100
    18.3 @@ -189,9 +189,8 @@
    18.4      val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
    18.5  
    18.6      fun print x =
    18.7 -      Pretty.from_ML
    18.8 -        (ML_Pretty.from_polyml
    18.9 -          (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)));
   18.10 +      Pretty.from_polyml
   18.11 +        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
   18.12      fun print_all () =
   18.13        #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
   18.14        |> sort_by #1 |> map (Pretty.item o single o print o #2)
    19.1 --- a/src/Pure/context.ML	Thu Mar 17 16:56:44 2016 +0100
    19.2 +++ b/src/Pure/context.ML	Fri Mar 18 16:26:35 2016 +0100
    19.3 @@ -169,6 +169,8 @@
    19.4  
    19.5  val pretty_thy = Pretty.str_list "{" "}" o display_names;
    19.6  
    19.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
    19.8 +
    19.9  fun pretty_abbrev_thy thy =
   19.10    let
   19.11      val names = display_names thy;
    20.1 --- a/src/Pure/morphism.ML	Thu Mar 17 16:56:44 2016 +0100
    20.2 +++ b/src/Pure/morphism.ML	Fri Mar 18 16:26:35 2016 +0100
    20.3 @@ -71,6 +71,8 @@
    20.4  
    20.5  fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
    20.6  
    20.7 +val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
    20.8 +
    20.9  fun binding (Morphism {binding, ...}) = apply binding;
   20.10  fun typ (Morphism {typ, ...}) = apply typ;
   20.11  fun term (Morphism {term, ...}) = apply term;