equal
deleted
inserted
replaced
44 |> (if ! O.quotes then quote else I) |
44 |> (if ! O.quotes then quote else I) |
45 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
45 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
46 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
46 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
47 end; |
47 end; |
48 |
48 |
|
49 fun output_ml ctxt src = |
|
50 if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
51 else |
|
52 split_lines |
|
53 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
|
54 #> space_implode "\\isasep\\isanewline%\n"; |
|
55 |
49 fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"; |
56 fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"; |
50 |
57 |
51 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
58 fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; |
52 |
59 |
53 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name); |
60 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name; Pretty.str name); |
90 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
97 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
91 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
98 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
92 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))), |
99 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))), |
93 ("named_thms", O.args (Scan.repeat (Attrib.thm -- |
100 ("named_thms", O.args (Scan.repeat (Attrib.thm -- |
94 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) |
101 Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) |
95 (output_named_list pretty_thm))]; |
102 (output_named_list pretty_thm)), |
|
103 ("ML_text", O.args (Scan.lift Args.name) output_ml)]; |
96 |
104 |
97 end; |
105 end; |