equal
deleted
inserted
replaced
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))))); |