src/Pure/ML/ml_antiquotation.ML
changeset 67146 909dcdec2122
parent 64556 851ae0e7b09c
child 69349 7cef9e386ffe
equal deleted inserted replaced
67145:e77c5bfca9aa 67146:909dcdec2122
    39       ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
    39       ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
    40 
    40 
    41   inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
    41   inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
    42 
    42 
    43   value (Binding.make ("binding", \<^here>))
    43   value (Binding.make ("binding", \<^here>))
    44     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    44     (Scan.lift (Parse.position Args.embedded) >> ML_Syntax.make_binding) #>
    45 
    45 
    46   value (Binding.make ("cartouche", \<^here>))
    46   value (Binding.make ("cartouche", \<^here>))
    47     (Scan.lift Args.cartouche_input >> (fn source =>
    47     (Scan.lift Args.cartouche_input >> (fn source =>
    48       "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
    48       "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
    49         ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
    49         ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));