50 |
50 |
51 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
51 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
52 |
52 |
53 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name false; Pretty.str name); |
53 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name false; Pretty.str name); |
54 |
54 |
|
55 |
|
56 (* theorems with names *) |
|
57 |
|
58 fun tweak_line s = |
|
59 if ! O.display then s else Symbol.strip_blanks s; |
|
60 |
|
61 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; |
|
62 |
|
63 fun output_named_list pretty src ctxt xs = |
|
64 map (apfst (pretty ctxt)) xs (*always pretty in order to exhibit errors!*) |
|
65 |> (if ! O.quotes then map (apfst Pretty.quote) else I) |
|
66 |> (if ! O.display then |
|
67 map (fn (p, name) => |
|
68 Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ |
|
69 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
70 #> space_implode "\\par\\smallskip%\n" |
|
71 #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
|
72 else |
|
73 map (fn (p, name) => |
|
74 Output.output (Pretty.str_of p) ^ |
|
75 "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}") |
|
76 #> space_implode "\\par\\smallskip%\n" |
|
77 #> enclose "\\isa{" "}"); |
|
78 |
|
79 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt; |
|
80 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
|
81 |
55 in |
82 in |
56 |
83 |
57 val _ = O.add_commands |
84 val _ = O.add_commands |
58 [("index_ML", arguments (index_ml "" ml_val)), |
85 [("index_ML", arguments (index_ml "" ml_val)), |
59 ("index_ML_type", arguments (index_ml "type" ml_type)), |
86 ("index_ML_type", arguments (index_ml "type" ml_type)), |
60 ("index_ML_exn", arguments (index_ml "exception" ml_exn)), |
87 ("index_ML_exn", arguments (index_ml "exception" ml_exn)), |
61 ("index_ML_structure", arguments (index_ml "structure" ml_structure)), |
88 ("index_ML_structure", arguments (index_ml "structure" ml_structure)), |
62 ("index_ML_functor", arguments (index_ml "functor" ml_functor)), |
89 ("index_ML_functor", arguments (index_ml "functor" ml_functor)), |
63 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
90 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
64 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
91 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
65 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))]; |
92 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))), |
|
93 ("named_thms", O.args (Scan.repeat (Attrib.thm -- |
|
94 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) |
|
95 (output_named_list pretty_thm))]; |
66 |
96 |
67 end; |
97 end; |