src/Pure/Tools/print_operation.ML
changeset 61223 dfccf6c06201
parent 61212 cb9d0c99bd36
child 64677 8dc24130e8fe
equal deleted inserted replaced
61222:05d28dc76e5c 61223:dfccf6c06201
    44     AList.update (op =) (name, (description, pr)) tab));
    44     AList.update (op =) (name, (description, pr)) tab));
    45   report ());
    45   report ());
    46 
    46 
    47 val _ =
    47 val _ =
    48   Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
    48   Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
    49     (fn {state, args, output_result} =>
    49     (fn {state, args, writeln_result, ...} =>
    50       let
    50       let
    51         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    51         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    52         fun err s = Pretty.mark_str (Markup.bad, s);
    52         fun err s = Pretty.mark_str (Markup.bad, s);
    53         fun print name =
    53         fun print name =
    54           (case AList.lookup (op =) (Synchronized.value print_operations) name of
    54           (case AList.lookup (op =) (Synchronized.value print_operations) name of
    55             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    55             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    56           | NONE => [err ("Unknown print operation: " ^ quote name)]);
    56           | NONE => [err ("Unknown print operation: " ^ quote name)]);
    57       in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    57       in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    58 
    58 
    59 end;
    59 end;
    60 
    60 
    61 
    61 
    62 (* common print operations *)
    62 (* common print operations *)