src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 27607 a21271f74bc7
parent 27604 6c347b96d941
child 27828 edafacb690a3
equal deleted inserted replaced
27606:82399f3a8ca8 27607:a21271f74bc7
    82 fun decorate bg en prfx =
    82 fun decorate bg en prfx =
    83   Output.writeln_default o enclose bg en o prefix_lines prfx;
    83   Output.writeln_default o enclose bg en o prefix_lines prfx;
    84 
    84 
    85 fun setup_messages () =
    85 fun setup_messages () =
    86  (Output.writeln_fn := Output.writeln_default;
    86  (Output.writeln_fn := Output.writeln_default;
    87   Output.status_fn := Output.writeln_default;
    87   Output.status_fn := (fn "" => () | s => ! Output.priority_fn s);
    88   Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
    88   Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
    89   Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
    89   Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
    90   Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
    90   Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
    91   Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
    91   Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
    92   Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
    92   Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);