src/Pure/Thy/document_antiquotations.ML
changeset 67188 bc7a6455e12a
parent 67184 ecc786cb3b7b
child 67194 1c0a6a957114
equal deleted inserted replaced
67187:3457d7d43ee9 67188:bc7a6455e12a
    43 local
    43 local
    44 
    44 
    45 fun control_antiquotation name s1 s2 =
    45 fun control_antiquotation name s1 s2 =
    46   Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
    46   Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
    47     (fn {state, ...} =>
    47     (fn {state, ...} =>
    48       enclose s1 s2 o Thy_Output.output_text state {markdown = false, mark_range = false});
    48       enclose s1 s2 o Thy_Output.output_text state {markdown = false, positions = false});
    49 
    49 
    50 in
    50 in
    51 
    51 
    52 val _ =
    52 val _ =
    53   Theory.setup
    53   Theory.setup