equal
deleted
inserted
replaced
13 |
13 |
14 structure Query_Operation: QUERY_OPERATION = |
14 structure Query_Operation: QUERY_OPERATION = |
15 struct |
15 struct |
16 |
16 |
17 fun register {name, pri} f = |
17 fun register {name, pri} f = |
18 Command.print_function name |
18 Command.print_function (name ^ "_query") |
19 (fn {args = instance :: args, ...} => |
19 (fn {args = instance :: args, ...} => |
20 SOME {delay = NONE, pri = pri, persistent = false, strict = false, |
20 SOME {delay = NONE, pri = pri, persistent = false, strict = false, |
21 print_fn = fn _ => uninterruptible (fn restore_attributes => fn state => |
21 print_fn = fn _ => uninterruptible (fn restore_attributes => fn state => |
22 let |
22 let |
23 fun result s = Output.result [(Markup.instanceN, instance)] [s]; |
23 fun result s = Output.result [(Markup.instanceN, instance)] [s]; |
35 val _ = status Markup.finished; |
35 val _ = status Markup.finished; |
36 in () end)} |
36 in () end)} |
37 | _ => NONE); |
37 | _ => NONE); |
38 |
38 |
39 end; |
39 end; |
40 |
|