src/Pure/Tools/print_operation.ML
changeset 60610 f52b4b0c10c4
parent 57605 8e0a7eaffe47
child 61212 cb9d0c99bd36
equal deleted inserted replaced
60609:15620ae824c0 60610:f52b4b0c10c4
    43     else warning ("Redefining print operation: " ^ quote name);
    43     else warning ("Redefining print operation: " ^ quote name);
    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 "print_operation" (fn {state, args, output_result} =>
    48   Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
    49     let
    49     (fn {state, args, output_result} =>
    50       val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    50       let
    51       fun err s = Pretty.mark_str (Markup.bad, s);
    51         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    52       fun print name =
    52         fun err s = Pretty.mark_str (Markup.bad, s);
    53         (case AList.lookup (op =) (Synchronized.value print_operations) name of
    53         fun print name =
    54           SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    54           (case AList.lookup (op =) (Synchronized.value print_operations) name of
    55         | NONE => [err ("Unknown print operation: " ^ quote name)]);
    55             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    56     in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    56           | NONE => [err ("Unknown print operation: " ^ quote name)]);
       
    57       in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    57 
    58 
    58 end;
    59 end;
    59 
    60 
    60 
    61 
    61 (* common print operations *)
    62 (* common print operations *)