src/Pure/Thy/thy_output.ML

   val defined_command: string -> bool
   val defined_option: string -> bool
   val print_antiquotations: unit -> unit
   val boolean: string -> bool
   val integer: string -> int
+  val raw_antiquotation: string -> (Args.src -> Toplevel.state ->
+    Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
+  val antiquotation: string -> (Args.src -> Proof.context ->
+    Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
   val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string

 
 
 (* args syntax *)
 
 fun syntax scan = Args.context_syntax "document antiquotation" scan;
+
+fun raw_antiquotation name scan =
+  add_commands [(name, fn src => fn state =>
+    #1 (syntax (scan src state) src (Toplevel.presentation_context_of state NONE)))];
+
+fun antiquotation name scan =
+  raw_antiquotation name (fn src => fn state =>
+    scan src (Toplevel.presentation_context_of state NONE));
 
 fun args scan f src state : string =
   let
     val loc = if ! locale = "" then NONE else SOME (! locale);
     val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);