moved @{ML_functor} and @{ML_text} to Pure;
adapted to simplified ThyOutput.antiquotation interface;
misc tuning;

--- a/doc-src/antiquote_setup.ML	Mon Mar 09 20:29:45 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Mar 09 20:34:11 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Doc/antiquote_setup.ML
+(*  Title:      doc-src/antiquote_setup.ML
     Author:     Makarius
 
 Auxiliary antiquotations for the Isabelle manuals.
@@ -52,87 +52,70 @@
 fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
   | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
 
-fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
+fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
 
-fun ml_functor _ = "val _ = ();";  (*no check!*)
+fun ml_functor _ = "";  (*no check!*)
 
-fun index_ml kind ml src ctxt (txt1, txt2) =
-  let
-    val txt = if txt2 = "" then txt1 else
-      if kind = "type" then txt1 ^ " = " ^ txt2
-      else if kind = "exception" then txt1 ^ " of " ^ txt2
-      else txt1 ^ ": " ^ txt2;
-    val txt' = if kind = "" then txt else kind ^ " " ^ txt;
-    val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
-    val kind' = if kind = "" then "ML" else "ML " ^ kind;
-  in
-    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
-    (txt'
-    |> (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 ! 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 = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
+fun index_ml name kind ml = ThyOutput.antiquotation name
+  (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
+  (fn {context = ctxt, ...} => fn (txt1, txt2) =>
+    let
+      val txt =
+        if txt2 = "" then txt1
+        else if kind = "type" then txt1 ^ " = " ^ txt2
+        else if kind = "exception" then txt1 ^ " of " ^ txt2
+        else txt1 ^ ": " ^ txt2;
+      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
+      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+      val kind' = if kind = "" then "ML" else "ML " ^ kind;
+    in
+      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
+      (txt'
+      |> (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);
 
 in
 
-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", ThyOutput.args (Scan.lift Args.name) output_ml),
-  ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
+val _ = index_ml "index_ML" "" ml_val;
+val _ = index_ml "index_ML_type" "type" ml_type;
+val _ = index_ml "index_ML_exn" "exception" ml_exn;
+val _ = index_ml "index_ML_structure" "structure" ml_structure;
+val _ = index_ml "index_ML_functor" "functor" ml_functor;
 
 end;
 
 
-(* theorems with names *)
-
-local
+(* named theorems *)
 
-fun output_named_thms src ctxt xs =
-  map (apfst (ThyOutput.pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
-  |> (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 (! 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}"
-  else
-    map (fn (p, name) =>
-      Output.output (Pretty.str_of p) ^
-      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
-    #> space_implode "\\par\\smallskip%\n"
-    #> enclose "\\isa{" "}");
-
-in
-
-val _ = ThyOutput.add_commands
- [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
-      Scan.lift (Args.parens Args.name))) output_named_thms)];
-
-end;
+val _ = ThyOutput.antiquotation "named_thms"
+  (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
+  (fn {context = ctxt, ...} =>
+    map (apfst (ThyOutput.pretty_thm ctxt))
+    #> (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 (! 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}"
+        else
+          map (fn (p, name) =>
+            Output.output (Pretty.str_of p) ^
+            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
+          #> space_implode "\\par\\smallskip%\n"
+          #> enclose "\\isa{" "}"));
 
 
-(* theory files *)
+(* theory file *)
 
-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))))];
+val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
+  (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
 
 
-(* Isabelle entities (with index) *)
+(* Isabelle/Isar entities (with index) *)
 
 local
 
@@ -147,56 +130,56 @@
 
 val arg = enclose "{" "}" o clean_string;
 
-fun output_entity check markup index kind ctxt (logic, name) =
-  let
-    val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
-    val hyper =
-      enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
-      index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
-    val idx =
-      (case index of
-        NONE => ""
-      | SOME is_def =>
-          "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
-  in
-    if check ctxt name then
-      idx ^
-      (Output.output name
-        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-        |> (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 =
-  ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
-    (K (output_entity check markup index kind));
+fun entity check markup kind index =
+  ThyOutput.antiquotation
+    (case index of NONE => kind | SOME true => kind ^ "_def" | SOME false => kind ^ "_ref")
+    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
+    (fn {context = ctxt, ...} => fn (logic, name) =>
+      let
+        val hyper_name =
+          "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
+        val hyper =
+          enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
+          index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
+        val idx =
+          (case index of
+            NONE => ""
+          | SOME is_def =>
+              "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
+      in
+        if check ctxt name then
+          idx ^
+          (Output.output name
+            |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
+            |> (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_antiqs check markup kind =
- [(kind, entity check markup NONE kind),
-  (kind ^ "_def", entity check markup (SOME true) kind),
-  (kind ^ "_ref", entity check markup (SOME false) kind)];
+ [(entity check markup kind NONE),
+  (entity check markup kind (SOME true)),
+  (entity check markup kind (SOME false))];
 
 in
 
-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" @
-  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
-  entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
-  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
-  entity_antiqs no_check "" "fact" @
-  entity_antiqs no_check "" "variable" @
-  entity_antiqs no_check "" "case" @
-  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
-  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
-  entity_antiqs no_check "" "inference" @
-  entity_antiqs no_check "isatt" "executable" @
-  entity_antiqs (K check_tool) "isatt" "tool" @
-  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
-  entity_antiqs (K ThyInfo.known_thy) "" "theory");
+val _ = entity_antiqs no_check "" "syntax";
+val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
+val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
+val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
+val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
+val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
+val _ = entity_antiqs no_check "" "fact";
+val _ = entity_antiqs no_check "" "variable";
+val _ = entity_antiqs no_check "" "case";
+val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
+val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
+val _ = entity_antiqs no_check "" "inference";
+val _ = entity_antiqs no_check "isatt" "executable";
+val _ = entity_antiqs (K check_tool) "isatt" "tool";
+val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
+val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
 
 end;
 

--- a/doc-src/more_antiquote.ML	Mon Mar 09 20:29:45 2009 +0100
+++ b/doc-src/more_antiquote.ML	Mon Mar 09 20:34:11 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Doc/more_antiquote.ML
+(*  Title:      doc-src/more_antiquote.ML
     Author:     Florian Haftmann, TU Muenchen
 
 More antiquotations.
@@ -12,15 +12,13 @@
 structure More_Antiquote : MORE_ANTIQUOTE =
 struct
 
-structure O = ThyOutput;
-
 (* printing typewriter lines *)
 
 fun typewriter s =
   let
     val parse = Scan.repeat
       (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
-        || (Scan.this_string " " 
+        || (Scan.this_string " "
           || Scan.this_string "."
           || Scan.this_string ","
           || Scan.this_string ":"
@@ -66,9 +64,8 @@
 
 in
 
-val _ = O.add_commands
-  [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
-    ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
+val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
+val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
 
 end;
 
@@ -96,12 +93,12 @@
     val thms = Code_Wellsorted.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
-  in ThyOutput.output_list pretty_thm src ctxt thms end;
+  in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
 
 in
 
-val _ = O.add_commands
-  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
+val _ = ThyOutput.antiquotation "code_thms" Args.term
+  (fn {source, context, ...} => pretty_code_thm source context);
 
 end;
 
@@ -120,21 +117,20 @@
     >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
   val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
     >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
-  val parse_names = parse_consts || parse_types || parse_classes || parse_instances; 
-
-  fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
-    Code_Target.code_of (ProofContext.theory_of ctxt)
-      target "Example" (mk_cs (ProofContext.theory_of ctxt))
-        (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
-    |> typewriter;
+  val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
 
 in
 
-val _ = O.add_commands
-  [("code_stmts", O.args
-      (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
-        code_stmts)]
-
-end
+val _ = ThyOutput.antiquotation "code_stmts"
+  (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
+  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
+    let val thy = ProofContext.theory_of ctxt in
+      Code_Target.code_of thy
+        target "Example" (mk_cs thy)
+        (fn naming => maps (fn f => f thy naming) mk_stmtss)
+      |> typewriter
+    end);
 
 end;
+
+end;

--- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:29:45 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:34:11 2009 +0100
@@ -590,8 +590,9 @@
 
 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
-val _ = ml_text "ML_struct"
-  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
+val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
+val _ = ml_text "ML_functor" (K "");  (*no check!*)
+val _ = ml_text "ML_text" (K "");
 
 end;