diff -r b83c75d051b7 -r a0b280dd4bc7 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Mon Jul 19 15:44:13 2010 +0100 +++ b/ProgTutorial/Tactical.thy Tue Jul 20 13:34:44 2010 +0100 @@ -252,7 +252,7 @@ ML{*fun my_print_tac ctxt thm = let - val _ = tracing (string_of_thm_no_vars ctxt thm) + val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm)) in Seq.single thm end*} @@ -544,24 +544,19 @@ ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = let - fun pairs1 f1 f2 xs = - commas (map (fn (x, y) => f1 x ^ ":=" ^ f2 y) xs) - - fun pairs2 f xs = pairs1 f f xs - - val string_of_params = pairs1 I (string_of_cterm context) params - val string_of_asms = string_of_cterms context asms - val string_of_concl = string_of_cterm context concl - val string_of_prems = string_of_thms_no_vars context prems - val string_of_schms = pairs2 (string_of_cterm context) (snd schematics) - - val strs = ["params: " ^ string_of_params, - "schematics: " ^ string_of_schms, - "assumptions: " ^ string_of_asms, - "conclusion: " ^ string_of_concl, - "premises: " ^ string_of_prems] + fun assgn1 f1 f2 xs = + Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) + + fun assgn2 f xs = assgn1 f f xs + + val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp]) + [("params: ", assgn1 Pretty.str (pretty_cterm context) params), + ("assumptions: ", pretty_cterms context asms), + ("conclusion: ", pretty_cterm context concl), + ("premises: ", pretty_thms_no_vars context prems), + ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))] in - tracing (cat_lines strs); all_tac + tracing (Pretty.string_of (Pretty.chunks pps)); all_tac end*} text_raw{* @@ -583,7 +578,7 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{text "x:=x"}, @{text "y:=y"}\\ + params: & @{text "x:= x"}, @{text "y:= y"}\\ schematics: & @{text "?z:=z"}\\ assumptions: & @{term "A x y"}\\ conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\ @@ -611,7 +606,7 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{text "x:=x"}, @{text "y:=y"}\\ + params: & @{text "x:= x"}, @{text "y:= y"}\\ schematics: & @{text "?z:=z"}\\ assumptions: & @{term "A x y"}, @{term "B y x"}\\ conclusion: & @{term "C (z y) x"}\\ @@ -1493,16 +1488,16 @@ val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss fun name_thm (nm, thm) = - " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) + Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm] fun name_ctrm (nm, ctrm) = - " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) - - val s = ["Simplification rules:"] @ map name_thm simps @ - ["Congruences rules:"] @ map name_thm congs @ - ["Simproc patterns:"] @ map name_ctrm procs + Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm] + + val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps), + Pretty.big_list "Congruences rules:" (map name_thm congs), + Pretty.big_list "Simproc patterns:" (map name_ctrm procs)] in - s |> cat_lines - |> tracing + pps |> Pretty.chunks + |> pwriteln end*} text_raw {* \end{isabelle}