src/Pure/PIDE/resources.ML
changeset 67464 a5ca98950a91
parent 67386 998e01d6f8fd
child 67472 bddfa23a4ea9
     1.1 --- a/src/Pure/PIDE/resources.ML	Thu Jan 18 21:29:28 2018 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Jan 18 21:41:30 2018 +0100
     1.3 @@ -243,12 +243,11 @@
     1.4    let
     1.5      val dir = master_directory (Proof_Context.theory_of ctxt);
     1.6      val _ = check ctxt dir (name, pos);
     1.7 -  in
     1.8 -    space_explode "/" name
     1.9 -    |> map Latex.output_ascii
    1.10 -    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
    1.11 -    |> enclose "\\isatt{" "}"
    1.12 -  end;
    1.13 +    val latex =
    1.14 +      space_explode "/" name
    1.15 +      |> map Latex.output_ascii
    1.16 +      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
    1.17 +  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
    1.18  
    1.19  fun ML_antiq check ctxt (name, pos) =
    1.20    let val path = check ctxt Path.current (name, pos);
    1.21 @@ -257,14 +256,14 @@
    1.22  in
    1.23  
    1.24  val _ = Theory.setup
    1.25 - (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
    1.26 -    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
    1.27 -  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
    1.28 -    (document_antiq check_path o #context) #>
    1.29 -  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
    1.30 -    (document_antiq check_file o #context) #>
    1.31 -  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
    1.32 -    (document_antiq check_dir o #context) #>
    1.33 + (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
    1.34 +    (Scan.lift (Parse.position Parse.embedded)) check_session #>
    1.35 +  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
    1.36 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
    1.37 +  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
    1.38 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
    1.39 +  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
    1.40 +    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
    1.41    ML_Antiquotation.value \<^binding>\<open>path\<close>
    1.42      (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
    1.43    ML_Antiquotation.value \<^binding>\<open>file\<close>