src/Pure/PIDE/query_operation.ML
changeset 61206 d5aeb401111a
parent 60610 f52b4b0c10c4
child 61208 19118f9b939d
equal deleted inserted replaced
61205:c0a5ebecc68b 61206:d5aeb401111a
    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