tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
authorwenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692ecd34f863242
parent 51691 69e3bc394f09
child 51693 1eb533ea1480
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
src/HOL/HOL.thy
src/HOL/Inductive.thy
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 10 20:58:01 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 10 21:20:35 2013 +0200
     1.3 @@ -8,8 +8,7 @@
     1.4  imports Pure "~~/src/Tools/Code_Generator"
     1.5  keywords
     1.6    "try" "solve_direct" "quickcheck"
     1.7 -    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" 
     1.8 -    "print_case_translations":: diag and
     1.9 +    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
    1.10    "quickcheck_params" :: thy_decl
    1.11  begin
    1.12  
     2.1 --- a/src/HOL/Inductive.thy	Wed Apr 10 20:58:01 2013 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Wed Apr 10 21:20:35 2013 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  keywords
     2.5    "inductive" "coinductive" :: thy_decl and
     2.6    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
     2.7 -  "print_inductives" :: diag and
     2.8 +  "print_inductives" "print_case_translations" :: diag and
     2.9    "rep_datatype" :: thy_goal and
    2.10    "primrec" :: thy_decl
    2.11  begin
     3.1 --- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 20:58:01 2013 +0200
     3.2 +++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 21:20:35 2013 +0200
     3.3 @@ -582,15 +582,15 @@
     3.4    let
     3.5      val cases = Symtab.dest (cases_of ctxt);
     3.6      fun show_case (_, data as (comb, ctrs)) =
     3.7 -      Pretty.big_list
     3.8 -        (Pretty.string_of (Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"]))
     3.9 -        [Pretty.block [Pretty.brk 3, Pretty.block
    3.10 +      (Pretty.block o Pretty.fbreaks)
    3.11 +        [Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"],
    3.12 +         Pretty.block [Pretty.brk 3, Pretty.block
    3.13            [Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]],
    3.14 -        Pretty.block [Pretty.brk 3, Pretty.block
    3.15 +         Pretty.block [Pretty.brk 3, Pretty.block
    3.16            [Pretty.str "constructors:", Pretty.brk 1,
    3.17 -             Pretty.list "" "" (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs)]]];
    3.18 +            Pretty.block (Pretty.commas (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs))]]];
    3.19    in
    3.20 -    Pretty.big_list "Case translations:" (map show_case cases)
    3.21 +    Pretty.big_list "case translations:" (map show_case cases)
    3.22      |> Pretty.writeln
    3.23    end;
    3.24