some shortcuts for chunks, which sometimes avoid bulky string output;
authorwenzelm
Mon Mar 31 12:35:39 2014 +0200 (2014-03-31 ago)
changeset 563346b3739fee456
parent 56333 38f1422ef473
child 56335 8953d4cc060a
some shortcuts for chunks, which sometimes avoid bulky string output;
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/HOL/Tools/inductive.ML
src/Provers/classical.ML
src/Pure/General/output.ML
src/Pure/General/pretty.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/toplevel.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Tools/Code/code_preproc.ML
src/Tools/induct.ML
src/Tools/subtyping.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 31 10:28:08 2014 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Mar 31 12:35:39 2014 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4           Pretty.big_list (name ^ " " ^ f status)
     1.5             (Element.pretty_ctxt ctxt context' @
     1.6              Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
     1.7 -    Pretty.chunks2 |> Pretty.writeln
     1.8 +    Pretty.writeln_chunks2
     1.9    end;
    1.10  
    1.11  val _ =
     2.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Mar 31 10:28:08 2014 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Mar 31 12:35:39 2014 +0200
     2.3 @@ -106,7 +106,7 @@
     2.4      [Pretty.str (msg ^ ":"), Pretty.str ""] @
     2.5      map pretty_thm with_superfluous_assumptions @
     2.6      [Pretty.str "", Pretty.str end_msg]
     2.7 -  end |> Pretty.chunks |> Pretty.writeln
     2.8 +  end |> Pretty.writeln_chunks
     2.9  
    2.10  end
    2.11  
     3.1 --- a/src/HOL/Tools/inductive.ML	Mon Mar 31 10:28:08 2014 +0200
     3.2 +++ b/src/HOL/Tools/inductive.ML	Mon Mar 31 12:35:39 2014 +0200
     3.3 @@ -232,7 +232,7 @@
     3.4          (Pretty.str "(co)inductives:" ::
     3.5            map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
     3.6       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
     3.7 -  end |> Pretty.chunks |> Pretty.writeln;
     3.8 +  end |> Pretty.writeln_chunks;
     3.9  
    3.10  
    3.11  (* inductive info *)
     4.1 --- a/src/Provers/classical.ML	Mon Mar 31 10:28:08 2014 +0200
     4.2 +++ b/src/Provers/classical.ML	Mon Mar 31 12:35:39 2014 +0200
     4.3 @@ -632,7 +632,7 @@
     4.4        Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
     4.5        Pretty.strs ("safe wrappers:" :: map #1 swrappers),
     4.6        Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
     4.7 -    |> Pretty.chunks |> Pretty.writeln
     4.8 +    |> Pretty.writeln_chunks
     4.9    end;
    4.10  
    4.11  
     5.1 --- a/src/Pure/General/output.ML	Mon Mar 31 10:28:08 2014 +0200
     5.2 +++ b/src/Pure/General/output.ML	Mon Mar 31 12:35:39 2014 +0200
     5.3 @@ -25,6 +25,7 @@
     5.4    val physical_stderr: output -> unit
     5.5    val physical_writeln: output -> unit
     5.6    exception Protocol_Message of Properties.T
     5.7 +  val writelns: string list -> unit
     5.8    val urgent_message: string -> unit
     5.9    val error_message': serial * string -> unit
    5.10    val error_message: string -> unit
    5.11 @@ -107,7 +108,8 @@
    5.12  val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
    5.13    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    5.14  
    5.15 -fun writeln s = ! writeln_fn [output s];
    5.16 +fun writelns ss = ! writeln_fn (map output ss);
    5.17 +fun writeln s = writelns [s];
    5.18  fun urgent_message s = ! urgent_message_fn [output s];  (*Proof General legacy*)
    5.19  fun tracing s = ! tracing_fn [output s];
    5.20  fun warning s = ! warning_fn [output s];
     6.1 --- a/src/Pure/General/pretty.ML	Mon Mar 31 10:28:08 2014 +0200
     6.2 +++ b/src/Pure/General/pretty.ML	Mon Mar 31 12:35:39 2014 +0200
     6.3 @@ -45,10 +45,6 @@
     6.4    val text: string -> T list
     6.5    val paragraph: T list -> T
     6.6    val para: string -> T
     6.7 -  val markup_chunks: Markup.T -> T list -> T
     6.8 -  val chunks: T list -> T
     6.9 -  val chunks2: T list -> T
    6.10 -  val block_enclose: T * T -> T list -> T
    6.11    val quote: T -> T
    6.12    val backquote: T -> T
    6.13    val cartouche: T -> T
    6.14 @@ -72,6 +68,12 @@
    6.15    val symbolic_output: T -> Output.output
    6.16    val symbolic_string_of: T -> string
    6.17    val str_of: T -> string
    6.18 +  val markup_chunks: Markup.T -> T list -> T
    6.19 +  val chunks: T list -> T
    6.20 +  val chunks2: T list -> T
    6.21 +  val block_enclose: T * T -> T list -> T
    6.22 +  val writeln_chunks: T list -> unit
    6.23 +  val writeln_chunks2: T list -> unit
    6.24    val to_ML: T -> ML_Pretty.pretty
    6.25    val from_ML: ML_Pretty.pretty -> T
    6.26  end;
    6.27 @@ -170,17 +172,6 @@
    6.28  val paragraph = markup Markup.paragraph;
    6.29  val para = paragraph o text;
    6.30  
    6.31 -fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
    6.32 -val chunks = markup_chunks Markup.empty;
    6.33 -
    6.34 -fun chunks2 prts =
    6.35 -  (case try split_last prts of
    6.36 -    NONE => blk (0, [])
    6.37 -  | SOME (prefix, last) =>
    6.38 -      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
    6.39 -
    6.40 -fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
    6.41 -
    6.42  fun quote prt = blk (1, [str "\"", prt, str "\""]);
    6.43  fun backquote prt = blk (1, [str "`", prt, str "`"]);
    6.44  fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
    6.45 @@ -355,6 +346,33 @@
    6.46  val str_of = Output.escape o Buffer.content o unformatted;
    6.47  
    6.48  
    6.49 +(* chunks *)
    6.50 +
    6.51 +fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
    6.52 +val chunks = markup_chunks Markup.empty;
    6.53 +
    6.54 +fun chunks2 prts =
    6.55 +  (case try split_last prts of
    6.56 +    NONE => blk (0, [])
    6.57 +  | SOME (prefix, last) =>
    6.58 +      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
    6.59 +
    6.60 +fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
    6.61 +
    6.62 +fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
    6.63 +
    6.64 +fun writeln_chunks prts =
    6.65 +  Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
    6.66 +
    6.67 +fun writeln_chunks2 prts =
    6.68 +  (case try split_last prts of
    6.69 +    NONE => ()
    6.70 +  | SOME (prefix, last) =>
    6.71 +      (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
    6.72 +        [string_of_text_fold last])
    6.73 +      |> Output.writelns);
    6.74 +
    6.75 +
    6.76  
    6.77  (** ML toplevel pretty printing **)
    6.78  
     7.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 31 10:28:08 2014 +0200
     7.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 31 12:35:39 2014 +0200
     7.3 @@ -105,7 +105,7 @@
     7.4              (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
     7.5    in
     7.6      [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
     7.7 -    |> Pretty.chunks |> Pretty.writeln
     7.8 +    |> Pretty.writeln_chunks
     7.9    end;
    7.10  
    7.11  val attribute_space = Name_Space.space_of_table o get_attributes o Context.Proof;
     8.1 --- a/src/Pure/Isar/bundle.ML	Mon Mar 31 10:28:08 2014 +0200
     8.2 +++ b/src/Pure/Isar/bundle.ML	Mon Mar 31 12:35:39 2014 +0200
     8.3 @@ -134,7 +134,7 @@
     8.4          Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
     8.5    in
     8.6      map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
     8.7 -  end |> Pretty.chunks |> Pretty.writeln;
     8.8 +  end |> Pretty.writeln_chunks;
     8.9  
    8.10  end;
    8.11  
     9.1 --- a/src/Pure/Isar/calculation.ML	Mon Mar 31 10:28:08 2014 +0200
     9.2 +++ b/src/Pure/Isar/calculation.ML	Mon Mar 31 12:35:39 2014 +0200
     9.3 @@ -46,7 +46,7 @@
     9.4    in
     9.5     [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
     9.6      Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
     9.7 -  end |> Pretty.chunks |> Pretty.writeln;
     9.8 +  end |> Pretty.writeln_chunks;
     9.9  
    9.10  
    9.11  (* access calculation *)
    10.1 --- a/src/Pure/Isar/class.ML	Mon Mar 31 10:28:08 2014 +0200
    10.2 +++ b/src/Pure/Isar/class.ML	Mon Mar 31 12:35:39 2014 +0200
    10.3 @@ -203,8 +203,7 @@
    10.4      Sorts.all_classes algebra
    10.5      |> sort (Name_Space.extern_ord ctxt class_space)
    10.6      |> map prt_entry
    10.7 -    |> Pretty.chunks2
    10.8 -    |> Pretty.writeln
    10.9 +    |> Pretty.writeln_chunks2
   10.10    end;
   10.11  
   10.12  
    11.1 --- a/src/Pure/Isar/code.ML	Mon Mar 31 10:28:08 2014 +0200
    11.2 +++ b/src/Pure/Isar/code.ML	Mon Mar 31 12:35:39 2014 +0200
    11.3 @@ -1036,7 +1036,7 @@
    11.4      val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
    11.5      val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
    11.6    in
    11.7 -    (Pretty.writeln o Pretty.chunks) [
    11.8 +    Pretty.writeln_chunks [
    11.9        Pretty.block (
   11.10          Pretty.str "code equations:" :: Pretty.fbrk
   11.11          :: (Pretty.fbreaks o map pretty_function) functions
    12.1 --- a/src/Pure/Isar/context_rules.ML	Mon Mar 31 10:28:08 2014 +0200
    12.2 +++ b/src/Pure/Isar/context_rules.ML	Mon Mar 31 12:35:39 2014 +0200
    12.3 @@ -120,7 +120,7 @@
    12.4          (map_filter (fn (_, (k, th)) =>
    12.5              if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
    12.6            (sort (int_ord o pairself fst) rules));
    12.7 -  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    12.8 +  in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
    12.9  
   12.10  
   12.11  (* access data *)
    13.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 31 10:28:08 2014 +0200
    13.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 31 12:35:39 2014 +0200
    13.3 @@ -333,7 +333,7 @@
    13.4          NONE => (Theory.parents_of thy, [thy])
    13.5        | SOME (xs, NONE) => (map get_theory xs, [thy])
    13.6        | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
    13.7 -    |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
    13.8 +    |> map pretty_thm |> Pretty.writeln_chunks
    13.9    end);
   13.10  
   13.11  
    14.1 --- a/src/Pure/Isar/method.ML	Mon Mar 31 10:28:08 2014 +0200
    14.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 31 12:35:39 2014 +0200
    14.3 @@ -328,7 +328,7 @@
    14.4              (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    14.5    in
    14.6      [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
    14.7 -    |> Pretty.chunks |> Pretty.writeln
    14.8 +    |> Pretty.writeln_chunks
    14.9    end;
   14.10  
   14.11  fun add_method name meth comment thy = thy
    15.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Mar 31 10:28:08 2014 +0200
    15.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 31 12:35:39 2014 +0200
    15.3 @@ -219,7 +219,7 @@
    15.4    dest_commands (#2 (get_syntax ()))
    15.5    |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
    15.6    |> map pretty_command
    15.7 -  |> Pretty.chunks |> Pretty.writeln;
    15.8 +  |> Pretty.writeln_chunks;
    15.9  
   15.10  fun print_outer_syntax () =
   15.11    let
   15.12 @@ -231,7 +231,7 @@
   15.13      [Pretty.strs ("syntax keywords:" :: map quote keywords),
   15.14        Pretty.big_list "commands:" (map pretty_command cmds),
   15.15        Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
   15.16 -    |> Pretty.chunks |> Pretty.writeln
   15.17 +    |> Pretty.writeln_chunks
   15.18    end;
   15.19  
   15.20  
    16.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 31 10:28:08 2014 +0200
    16.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Mar 31 12:35:39 2014 +0200
    16.3 @@ -1250,7 +1250,7 @@
    16.4      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
    16.5    end;
    16.6  
    16.7 -val print_abbrevs = Pretty.writeln o Pretty.chunks o pretty_abbrevs true;
    16.8 +val print_abbrevs = Pretty.writeln_chunks o pretty_abbrevs true;
    16.9  
   16.10  
   16.11  (* term bindings *)
   16.12 @@ -1264,7 +1264,7 @@
   16.13      else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   16.14    end;
   16.15  
   16.16 -val print_binds = Pretty.writeln o Pretty.chunks o pretty_binds;
   16.17 +val print_binds = Pretty.writeln_chunks o pretty_binds;
   16.18  
   16.19  
   16.20  (* local facts *)
   16.21 @@ -1284,7 +1284,7 @@
   16.22    end;
   16.23  
   16.24  fun print_local_facts ctxt verbose =
   16.25 -  Pretty.writeln (Pretty.chunks (pretty_local_facts ctxt verbose));
   16.26 +  Pretty.writeln_chunks (pretty_local_facts ctxt verbose);
   16.27  
   16.28  
   16.29  (* local contexts *)
   16.30 @@ -1331,7 +1331,7 @@
   16.31      else [Pretty.big_list "cases:" (map pretty_case cases)]
   16.32    end;
   16.33  
   16.34 -val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
   16.35 +val print_cases = Pretty.writeln_chunks o pretty_cases;
   16.36  
   16.37  end;
   16.38  
    17.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 31 10:28:08 2014 +0200
    17.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 31 12:35:39 2014 +0200
    17.3 @@ -205,7 +205,7 @@
    17.4    | SOME (Theory (gthy, _)) => pretty_context gthy
    17.5    | SOME (Proof (_, (_, gthy))) => pretty_context gthy
    17.6    | SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy)
    17.7 -  |> Pretty.chunks |> Pretty.writeln;
    17.8 +  |> Pretty.writeln_chunks;
    17.9  
   17.10  fun print_state prf_only state =
   17.11    (case try node_of state of
    18.1 --- a/src/Pure/Syntax/syntax.ML	Mon Mar 31 10:28:08 2014 +0200
    18.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Mar 31 12:35:39 2014 +0200
    18.3 @@ -575,9 +575,9 @@
    18.4  
    18.5  in
    18.6  
    18.7 -fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
    18.8 -fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
    18.9 -fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
   18.10 +fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
   18.11 +fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
   18.12 +fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
   18.13  
   18.14  end;
   18.15  
    19.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon Mar 31 10:28:08 2014 +0200
    19.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Mar 31 12:35:39 2014 +0200
    19.3 @@ -878,7 +878,7 @@
    19.4      pretty_checks "term_checks" term_checks @
    19.5      pretty_checks "typ_unchecks" typ_unchecks @
    19.6      pretty_checks "term_unchecks" term_unchecks
    19.7 -  end |> Pretty.chunks |> Pretty.writeln;
    19.8 +  end |> Pretty.writeln_chunks;
    19.9  
   19.10  
   19.11  local
    20.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 31 10:28:08 2014 +0200
    20.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 31 12:35:39 2014 +0200
    20.3 @@ -109,7 +109,7 @@
    20.4    in
    20.5      [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
    20.6        Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
    20.7 -    |> Pretty.chunks |> Pretty.writeln
    20.8 +    |> Pretty.writeln_chunks
    20.9    end;
   20.10  
   20.11  fun antiquotation name scan body =
    21.1 --- a/src/Tools/Code/code_preproc.ML	Mon Mar 31 10:28:08 2014 +0200
    21.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Mar 31 12:35:39 2014 +0200
    21.3 @@ -181,7 +181,7 @@
    21.4      val post = (#post o the_thmproc) thy;
    21.5      val functrans = (map fst o #functrans o the_thmproc) thy;
    21.6    in
    21.7 -    (Pretty.writeln o Pretty.chunks) [
    21.8 +    Pretty.writeln_chunks [
    21.9        Pretty.block [
   21.10          Pretty.str "preprocessing simpset:",
   21.11          Pretty.fbrk,
    22.1 --- a/src/Tools/induct.ML	Mon Mar 31 10:28:08 2014 +0200
    22.2 +++ b/src/Tools/induct.ML	Mon Mar 31 12:35:39 2014 +0200
    22.3 @@ -254,7 +254,7 @@
    22.4      pretty_rules ctxt "induct pred:" inductP,
    22.5      pretty_rules ctxt "cases type:" casesT,
    22.6      pretty_rules ctxt "cases pred:" casesP]
    22.7 -    |> Pretty.chunks |> Pretty.writeln
    22.8 +    |> Pretty.writeln_chunks
    22.9    end;
   22.10  
   22.11  val _ =
    23.1 --- a/src/Tools/subtyping.ML	Mon Mar 31 10:28:08 2014 +0200
    23.2 +++ b/src/Tools/subtyping.ML	Mon Mar 31 12:35:39 2014 +0200
    23.3 @@ -1085,7 +1085,7 @@
    23.4     [Pretty.big_list "coercions between base types:" (map show_coercion simple),
    23.5      Pretty.big_list "other coercions:" (map show_coercion complex),
    23.6      Pretty.big_list "coercion maps:" (map show_map tmaps)]
    23.7 -  end |> Pretty.chunks |> Pretty.writeln;
    23.8 +  end |> Pretty.writeln_chunks;
    23.9  
   23.10  
   23.11  (* theory setup *)