# HG changeset patch # User wenzelm # Date 1236544539 -3600 # Node ID 937eaec692cb29b37c3c827496311d1083744792 # Parent 1a2a54f910c98bfbcaa226b8638652025975baaf use simplified ThyOutput.antiquotation; eliminated obscure structure alias; diff -r 1a2a54f910c9 -r 937eaec692cb doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Sun Mar 08 21:12:37 2009 +0100 +++ b/doc-src/antiquote_setup.ML Sun Mar 08 21:35:39 2009 +0100 @@ -7,9 +7,6 @@ structure AntiquoteSetup: sig end = struct -structure O = ThyOutput; - - (* misc utils *) fun translate f = Symbol.explode #> map f #> implode; @@ -38,9 +35,8 @@ val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; -val _ = O.add_commands - [("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ => - split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))]; +val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ => + Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")); (* ML text *) @@ -72,30 +68,30 @@ in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^ (txt' - |> (if ! O.quotes then quote else I) - |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" + |> (if ! ThyOutput.quotes then quote else I) + |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) end; fun output_ml ctxt src = - if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" + if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" else split_lines #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") #> space_implode "\\isasep\\isanewline%\n"; -fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; +fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x; in -val _ = O.add_commands +val _ = ThyOutput.add_commands [("index_ML", ml_args (index_ml "" ml_val)), ("index_ML_type", ml_args (index_ml "type" ml_type)), ("index_ML_exn", ml_args (index_ml "exception" ml_exn)), ("index_ML_structure", ml_args (index_ml "structure" ml_structure)), ("index_ML_functor", ml_args (index_ml "functor" ml_functor)), - ("ML_functor", O.args (Scan.lift Args.name) output_ml), - ("ML_text", O.args (Scan.lift Args.name) output_ml)]; + ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml), + ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)]; end; @@ -106,10 +102,10 @@ fun output_named_thms src ctxt xs = map (apfst (ThyOutput.pretty_thm ctxt)) xs (*always pretty in order to exhibit errors!*) - |> (if ! O.quotes then map (apfst Pretty.quote) else I) - |> (if ! O.display then + |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I) + |> (if ! ThyOutput.display then map (fn (p, name) => - Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^ + Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^ "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}") #> space_implode "\\par\\smallskip%\n" #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" @@ -122,8 +118,8 @@ in -val _ = O.add_commands - [("named_thms", O.args (Scan.repeat (Attrib.thm -- +val _ = ThyOutput.add_commands + [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) output_named_thms)]; end; @@ -131,8 +127,8 @@ (* theory files *) -val _ = O.add_commands - [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => +val _ = ThyOutput.add_commands + [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name => (ThyLoad.check_thy Path.current name; Pretty.str name))))]; @@ -167,14 +163,14 @@ idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") - |> (if ! O.quotes then quote else I) - |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" + |> (if ! ThyOutput.quotes then quote else I) + |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" else hyper o enclose "\\mbox{\\isa{" "}}")) else error ("Bad " ^ kind ^ " " ^ quote name) end; fun entity check markup index kind = - O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) + ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name)) (K (output_entity check markup index kind)); fun entity_antiqs check markup kind = @@ -184,7 +180,7 @@ in -val _ = O.add_commands +val _ = ThyOutput.add_commands (entity_antiqs no_check "" "syntax" @ entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @ entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @