tuned message -- more markup;
authorwenzelm
Sun Jun 23 22:31:50 2013 +0200 (2013-06-23)
changeset 52432c03090937c3b
parent 52431 7fa1245f50df
child 52433 ec3a22e62b54
tuned message -- more markup;
etc/isar-keywords.el
src/HOL/HOL.thy
src/Tools/subtyping.ML
     1.1 --- a/etc/isar-keywords.el	Sun Jun 23 21:40:56 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Sun Jun 23 22:31:50 2013 +0200
     1.3 @@ -183,7 +183,6 @@
     1.4      "print_classes"
     1.5      "print_codeproc"
     1.6      "print_codesetup"
     1.7 -    "print_coercion_maps"
     1.8      "print_coercions"
     1.9      "print_commands"
    1.10      "print_context"
    1.11 @@ -413,7 +412,6 @@
    1.12      "print_classes"
    1.13      "print_codeproc"
    1.14      "print_codesetup"
    1.15 -    "print_coercion_maps"
    1.16      "print_coercions"
    1.17      "print_commands"
    1.18      "print_context"
     2.1 --- a/src/HOL/HOL.thy	Sun Jun 23 21:40:56 2013 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Jun 23 22:31:50 2013 +0200
     2.3 @@ -7,8 +7,8 @@
     2.4  theory HOL
     2.5  imports Pure "~~/src/Tools/Code_Generator"
     2.6  keywords
     2.7 -  "try" "solve_direct" "quickcheck"
     2.8 -    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
     2.9 +  "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
    2.10 +    "print_induct_rules" :: diag and
    2.11    "quickcheck_params" :: thy_decl
    2.12  begin
    2.13  
     3.1 --- a/src/Tools/subtyping.ML	Sun Jun 23 21:40:56 2013 +0200
     3.2 +++ b/src/Tools/subtyping.ML	Sun Jun 23 22:31:50 2013 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4    val add_type_map: term -> Context.generic -> Context.generic
     3.5    val add_coercion: term -> Context.generic -> Context.generic
     3.6    val print_coercions: Proof.context -> unit
     3.7 -  val print_coercion_maps: Proof.context -> unit
     3.8    val setup: theory -> theory
     3.9  end;
    3.10  
    3.11 @@ -26,7 +25,7 @@
    3.12    {coes: (term * ((typ list * typ list) * term list)) Symreltab.table,  (*coercions table*)
    3.13     (*full coercions graph - only used at coercion declaration/deletion*)
    3.14     full_graph: int Graph.T,
    3.15 -   (*coercions graph restricted to base types - for efficiency reasons strored in the context*)
    3.16 +   (*coercions graph restricted to base types - for efficiency reasons stored in the context*)
    3.17     coes_graph: int Graph.T,
    3.18     tmaps: (term * variance list) Symtab.table,  (*map functions*)
    3.19     coerce_args: coerce_arg list Symtab.table  (*special constants with non-coercible arguments*)};
    3.20 @@ -326,7 +325,7 @@
    3.21              val tye_idx'' = strong_unify ctxt (U --> V, T) (tye, idx + 2)
    3.22                handle NO_UNIFIER (msg, _) => error (gen_msg err msg);
    3.23              val error_pack = (bs, t $ u, U, V, U');
    3.24 -          in 
    3.25 +          in
    3.26              if coerce'
    3.27              then (V, tye_idx'', ((U', U), error_pack) :: cs'')
    3.28              else (V,
    3.29 @@ -820,7 +819,7 @@
    3.30                      (if coerce' then "\nLocal coercion insertion on the operand failed:\n"
    3.31                      else "\nLocal coercion insertion on the operand disallowed:\n");
    3.32                    val (u'', U', tye_idx') =
    3.33 -                    if coerce' then 
    3.34 +                    if coerce' then
    3.35                        let val co = gen_coercion ctxt err' tye' (U, W);
    3.36                        in inf coerce' bs (if is_identity co then u else co $ u) (tye', idx') end
    3.37                      else (u, U, (tye', idx'));
    3.38 @@ -1030,32 +1029,33 @@
    3.39  fun print_coercions ctxt =
    3.40    let
    3.41      fun separate _ [] = ([], [])
    3.42 -      | separate P (x::xs) = (if P x then apfst else apsnd) (cons x) (separate P xs);
    3.43 +      | separate P (x :: xs) = (if P x then apfst else apsnd) (cons x) (separate P xs);
    3.44      val (simple, complex) =
    3.45        separate (fn (_, (_, ((Ts, Us), _))) => null Ts andalso null Us)
    3.46          (Symreltab.dest (coes_of ctxt));
    3.47 -    fun show_coercion ((a, b), (t, ((Ts, Us), _))) = Pretty.block [
    3.48 -      Syntax.pretty_typ ctxt (Type (a, Ts)),
    3.49 -      Pretty.brk 1, Pretty.str "<:", Pretty.brk 1,
    3.50 -      Syntax.pretty_typ ctxt (Type (b, Us)),
    3.51 -      Pretty.brk 3, Pretty.block [Pretty.str "using", Pretty.brk 1,
    3.52 -      Pretty.quote (Syntax.pretty_term ctxt t)]];
    3.53 +    fun show_coercion ((a, b), (t, ((Ts, Us), _))) =
    3.54 +      Pretty.item [Pretty.block
    3.55 +       [Syntax.pretty_typ ctxt (Type (a, Ts)), Pretty.brk 1,
    3.56 +        Pretty.str "<:", Pretty.brk 1,
    3.57 +        Syntax.pretty_typ ctxt (Type (b, Us)), Pretty.brk 3,
    3.58 +        Pretty.block
    3.59 +         [Pretty.keyword "using", Pretty.brk 1,
    3.60 +          Pretty.quote (Syntax.pretty_term ctxt t)]]];
    3.61 +
    3.62 +    val type_space = Proof_Context.type_space ctxt;
    3.63 +    val tmaps =
    3.64 +      sort (Name_Space.extern_ord ctxt type_space o pairself #1)
    3.65 +        (Symtab.dest (tmaps_of ctxt));
    3.66 +    fun show_map (x, (t, _)) =
    3.67 +      Pretty.block
    3.68 +       [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
    3.69 +        Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
    3.70    in
    3.71 -    Pretty.big_list "Coercions:"
    3.72 -    [Pretty.big_list "between base types:" (map show_coercion simple),
    3.73 -     Pretty.big_list "other:" (map show_coercion complex)]
    3.74 -    |> Pretty.writeln
    3.75 -  end;
    3.76 +   [Pretty.big_list "coercions between base types:" (map show_coercion simple),
    3.77 +    Pretty.big_list "other coercions:" (map show_coercion complex),
    3.78 +    Pretty.big_list "coercion maps:" (map show_map tmaps)]
    3.79 +  end |> Pretty.chunks |> Pretty.writeln;
    3.80  
    3.81 -fun print_coercion_maps ctxt =
    3.82 -  let
    3.83 -    fun show_map (x, (t, _)) = Pretty.block [
    3.84 -      Pretty.str x, Pretty.str ":", Pretty.brk 1,
    3.85 -      Pretty.quote (Syntax.pretty_term ctxt t)];
    3.86 -  in
    3.87 -    Pretty.big_list "Coercion maps:" (map show_map (Symtab.dest (tmaps_of ctxt)))
    3.88 -    |> Pretty.writeln
    3.89 -  end;
    3.90  
    3.91  (* theory setup *)
    3.92  
    3.93 @@ -1082,10 +1082,8 @@
    3.94  (* outer syntax commands *)
    3.95  
    3.96  val _ =
    3.97 -  Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
    3.98 -    (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
    3.99 -val _ =
   3.100 -  Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
   3.101 -    (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
   3.102 +  Outer_Syntax.improper_command @{command_spec "print_coercions"}
   3.103 +    "print information about coercions"
   3.104 +    (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)));
   3.105  
   3.106  end;