equal
deleted
inserted
replaced
37 (declaration (Binding.make ("here", @{here})) (Scan.succeed ()) |
37 (declaration (Binding.make ("here", @{here})) (Scan.succeed ()) |
38 (fn src => fn () => |
38 (fn src => fn () => |
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})) |
41 inline (Binding.make ("make_string", @{here})) |
42 (Args.context >> (ML_Pretty.make_string_fn o ML_Context.struct_name)) #> |
42 (Args.context >> (ML_Pretty.make_string_local o ML_Context.struct_name)) #> |
43 |
43 |
44 value (Binding.make ("binding", @{here})) |
44 value (Binding.make ("binding", @{here})) |
45 (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> |
45 (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> |
46 |
46 |
47 value (Binding.make ("cartouche", @{here})) |
47 value (Binding.make ("cartouche", @{here})) |