1.1 --- a/doc-src/antiquote_setup.ML	Sun Mar 08 21:12:37 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Sun Mar 08 21:35:39 2009 +0100
     1.3 @@ -7,9 +7,6 @@
     1.4  structure AntiquoteSetup: sig end =
     1.5  struct
     1.6  
     1.7 -structure O = ThyOutput;
     1.8 -
     1.9 -
    1.10  (* misc utils *)
    1.11  
    1.12  fun translate f = Symbol.explode #> map f #> implode;
    1.13 @@ -38,9 +35,8 @@
    1.14  
    1.15  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    1.16  
    1.17 -val _ = O.add_commands
    1.18 - [("verbatim", O.args (Scan.lift Args.name) (fn _ => fn _ =>
    1.19 -      split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))];
    1.20 +val _ = ThyOutput.antiquotation "verbatim" (fn _ => fn _ =>
    1.21 +  Scan.lift Args.name >> (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
    1.22  
    1.23  
    1.24  (* ML text *)
    1.25 @@ -72,30 +68,30 @@
    1.26    in
    1.27      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.28      (txt'
    1.29 -    |> (if ! O.quotes then quote else I)
    1.30 -    |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.31 +    |> (if ! ThyOutput.quotes then quote else I)
    1.32 +    |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.33          else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.34    end;
    1.35  
    1.36  fun output_ml ctxt src =
    1.37 -  if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.38 +  if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.39    else
    1.40      split_lines
    1.41      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    1.42      #> space_implode "\\isasep\\isanewline%\n";
    1.43  
    1.44 -fun ml_args x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
    1.45 +fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
    1.46  
    1.47  in
    1.48  
    1.49 -val _ = O.add_commands
    1.50 +val _ = ThyOutput.add_commands
    1.51   [("index_ML", ml_args (index_ml "" ml_val)),
    1.52    ("index_ML_type", ml_args (index_ml "type" ml_type)),
    1.53    ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
    1.54    ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
    1.55    ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
    1.56 -  ("ML_functor", O.args (Scan.lift Args.name) output_ml),
    1.57 -  ("ML_text", O.args (Scan.lift Args.name) output_ml)];
    1.58 +  ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml),
    1.59 +  ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
    1.60  
    1.61  end;
    1.62  
    1.63 @@ -106,10 +102,10 @@
    1.64  
    1.65  fun output_named_thms src ctxt xs =
    1.66    map (apfst (ThyOutput.pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
    1.67 -  |> (if ! O.quotes then map (apfst Pretty.quote) else I)
    1.68 -  |> (if ! O.display then
    1.69 +  |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
    1.70 +  |> (if ! ThyOutput.display then
    1.71      map (fn (p, name) =>
    1.72 -      Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
    1.73 +      Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
    1.74        "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.75      #> space_implode "\\par\\smallskip%\n"
    1.76      #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.77 @@ -122,8 +118,8 @@
    1.78  
    1.79  in
    1.80  
    1.81 -val _ = O.add_commands
    1.82 - [("named_thms", O.args (Scan.repeat (Attrib.thm --
    1.83 +val _ = ThyOutput.add_commands
    1.84 + [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
    1.85        Scan.lift (Args.parens Args.name))) output_named_thms)];
    1.86  
    1.87  end;
    1.88 @@ -131,8 +127,8 @@
    1.89  
    1.90  (* theory files *)
    1.91  
    1.92 -val _ = O.add_commands
    1.93 - [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
    1.94 +val _ = ThyOutput.add_commands
    1.95 + [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name =>
    1.96        (ThyLoad.check_thy Path.current name; Pretty.str name))))];
    1.97  
    1.98  
    1.99 @@ -167,14 +163,14 @@
   1.100        idx ^
   1.101        (Output.output name
   1.102          |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   1.103 -        |> (if ! O.quotes then quote else I)
   1.104 -        |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.105 +        |> (if ! ThyOutput.quotes then quote else I)
   1.106 +        |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.107              else hyper o enclose "\\mbox{\\isa{" "}}"))
   1.108      else error ("Bad " ^ kind ^ " " ^ quote name)
   1.109    end;
   1.110  
   1.111  fun entity check markup index kind =
   1.112 -  O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   1.113 +  ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   1.114      (K (output_entity check markup index kind));
   1.115  
   1.116  fun entity_antiqs check markup kind =
   1.117 @@ -184,7 +180,7 @@
   1.118  
   1.119  in
   1.120  
   1.121 -val _ = O.add_commands
   1.122 +val _ = ThyOutput.add_commands
   1.123   (entity_antiqs no_check "" "syntax" @
   1.124    entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
   1.125    entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @