src/Pure/Isar/isar_output.ML
changeset 14345 3023d90dc59e
parent 13929 21615e44ba88
child 14696 e862cc138e9c
     1.1 --- a/src/Pure/Isar/isar_output.ML	Thu Jan 08 04:32:52 2004 +0100
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Jan 08 08:14:00 2004 +0100
     1.3 @@ -287,6 +287,18 @@
     1.4      (if ! break then Pretty.string_of else Pretty.str_of) prt
     1.5      |> enclose "\\isa{" "}";
     1.6  
     1.7 +fun cond_seq_display prts =
     1.8 +  if ! display then
     1.9 +    map (Pretty.string_of o Pretty.indent (! indent)) prts
    1.10 +    |> separate "\\isasep\\isanewline%\n"
    1.11 +    |> implode
    1.12 +    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.13 +  else
    1.14 +    map (if ! break then Pretty.string_of else Pretty.str_of) prts
    1.15 +    |> separate "\\isasep\\isanewline%\n"
    1.16 +    |> implode
    1.17 +    |> enclose "\\isa{" "}";
    1.18 +
    1.19  fun tweak_line s =
    1.20    if ! display then s else Symbol.strip_blanks s;
    1.21  
    1.22 @@ -297,8 +309,7 @@
    1.23  
    1.24  fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
    1.25  
    1.26 -fun pretty_thms ctxt thms =
    1.27 -  Pretty.chunks (map (pretty_term ctxt o Thm.prop_of) thms);
    1.28 +fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    1.29  
    1.30  fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
    1.31    Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
    1.32 @@ -309,13 +320,19 @@
    1.33      val prt' = if ! source then pretty_source src else prt;
    1.34    in cond_display (cond_quote prt') end;
    1.35  
    1.36 +fun output_seq_with pretty src ctxt xs =
    1.37 +  let
    1.38 +    val prts = map (pretty ctxt) xs;   (*always pretty in order to catch errors!*)
    1.39 +    val prts' = if ! source then [pretty_source src] else prts;
    1.40 +  in cond_seq_display (map cond_quote prts') end;
    1.41 +
    1.42  fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
    1.43    Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
    1.44        handle Toplevel.UNDEF => error "No proof state")))) src state;
    1.45  
    1.46  val _ = add_commands
    1.47   [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
    1.48 -  ("thm", args Attrib.local_thmss (output_with pretty_thms)),
    1.49 +  ("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
    1.50    ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
    1.51    ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
    1.52    ("prop", args Args.local_prop (output_with pretty_term)),