equal
deleted
inserted
replaced
50 |
50 |
51 |
51 |
52 (** misc antiquotations **) |
52 (** misc antiquotations **) |
53 |
53 |
54 val _ = Theory.setup |
54 val _ = Theory.setup |
55 (inline (Binding.name "assert") |
55 (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ()) |
|
56 (fn src => fn () => fn ctxt => |
|
57 let |
|
58 val (a, ctxt') = variant "position" ctxt; |
|
59 val (_, pos) = Args.name_of_src src; |
|
60 val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; |
|
61 val body = "Isabelle." ^ a; |
|
62 in (K (env, body), ctxt') end) #> |
|
63 |
|
64 inline (Binding.name "assert") |
56 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
65 (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> |
57 |
66 |
58 inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> |
67 inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> |
59 |
68 |
60 value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) => |
69 value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) => |