equal
deleted
inserted
replaced
57 |
57 |
58 val value = declaration "val"; |
58 val value = declaration "val"; |
59 |
59 |
60 |
60 |
61 |
61 |
62 (** concrete antiquotations **) |
62 (** misc antiquotations **) |
63 |
63 |
64 structure P = OuterParse; |
64 structure P = OuterParse; |
65 |
65 |
66 |
66 val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b => |
67 (* misc *) |
67 ML_Syntax.atomic ("Binding.make " ^ |
|
68 ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b))); |
68 |
69 |
69 val _ = value "theory" |
70 val _ = value "theory" |
70 (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name) |
71 (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name) |
71 || Scan.succeed "ML_Context.the_global_context ()"); |
72 || Scan.succeed "ML_Context.the_global_context ()"); |
72 |
73 |