src/Pure/PIDE/resources.ML

 
 fun document_antiq check ctxt (name, pos) =
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
     val _ = check ctxt dir (name, pos);
-  in
-    space_explode "/" name
-    |> map Latex.output_ascii
-    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
-    |> enclose "\\isatt{" "}"
-  end;
+    val latex =
+      space_explode "/" name
+      |> map Latex.output_ascii
+      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
+  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
 
 fun ML_antiq check ctxt (name, pos) =
   let val path = check ctxt Path.current (name, pos);
   in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
 
 in
 
 val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
-    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
-  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_path o #context) #>
-  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_file o #context) #>
-  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_dir o #context) #>
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
+    (Scan.lift (Parse.position Parse.embedded)) check_session #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
   ML_Antiquotation.value \<^binding>\<open>path\<close>
     (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
   ML_Antiquotation.value \<^binding>\<open>file\<close>
     (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_file)) #>
   ML_Antiquotation.value \<^binding>\<open>dir\<close>