separate thm lists in latex output by \isasep
authorkleing
Thu Jan 08 08:14:00 2004 +0100 (2004-01-08)
changeset 143453023d90dc59e
parent 14344 0f0a2148a099
child 14346 5b9dd0de05d0
separate thm lists in latex output by \isasep
lib/texinputs/isabelle.sty
src/Pure/Isar/isar_output.ML
     1.1 --- a/lib/texinputs/isabelle.sty	Thu Jan 08 04:32:52 2004 +0100
     1.2 +++ b/lib/texinputs/isabelle.sty	Thu Jan 08 08:14:00 2004 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4  
     1.5  \newcommand{\isaindent}[1]{\hphantom{#1}}
     1.6  \newcommand{\isanewline}{\mbox{}\par\mbox{}}
     1.7 +\newcommand{\isasep}{\vspace*{2cm}}
     1.8  \newcommand{\isadigit}[1]{#1}
     1.9  
    1.10  \chardef\isacharbang=`\!
     2.1 --- a/src/Pure/Isar/isar_output.ML	Thu Jan 08 04:32:52 2004 +0100
     2.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Jan 08 08:14:00 2004 +0100
     2.3 @@ -287,6 +287,18 @@
     2.4      (if ! break then Pretty.string_of else Pretty.str_of) prt
     2.5      |> enclose "\\isa{" "}";
     2.6  
     2.7 +fun cond_seq_display prts =
     2.8 +  if ! display then
     2.9 +    map (Pretty.string_of o Pretty.indent (! indent)) prts
    2.10 +    |> separate "\\isasep\\isanewline%\n"
    2.11 +    |> implode
    2.12 +    |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    2.13 +  else
    2.14 +    map (if ! break then Pretty.string_of else Pretty.str_of) prts
    2.15 +    |> separate "\\isasep\\isanewline%\n"
    2.16 +    |> implode
    2.17 +    |> enclose "\\isa{" "}";
    2.18 +
    2.19  fun tweak_line s =
    2.20    if ! display then s else Symbol.strip_blanks s;
    2.21  
    2.22 @@ -297,8 +309,7 @@
    2.23  
    2.24  fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
    2.25  
    2.26 -fun pretty_thms ctxt thms =
    2.27 -  Pretty.chunks (map (pretty_term ctxt o Thm.prop_of) thms);
    2.28 +fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    2.29  
    2.30  fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
    2.31    Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
    2.32 @@ -309,13 +320,19 @@
    2.33      val prt' = if ! source then pretty_source src else prt;
    2.34    in cond_display (cond_quote prt') end;
    2.35  
    2.36 +fun output_seq_with pretty src ctxt xs =
    2.37 +  let
    2.38 +    val prts = map (pretty ctxt) xs;   (*always pretty in order to catch errors!*)
    2.39 +    val prts' = if ! source then [pretty_source src] else prts;
    2.40 +  in cond_seq_display (map cond_quote prts') end;
    2.41 +
    2.42  fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
    2.43    Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
    2.44        handle Toplevel.UNDEF => error "No proof state")))) src state;
    2.45  
    2.46  val _ = add_commands
    2.47   [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
    2.48 -  ("thm", args Attrib.local_thmss (output_with pretty_thms)),
    2.49 +  ("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
    2.50    ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
    2.51    ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))),
    2.52    ("prop", args Args.local_prop (output_with pretty_term)),