equal
deleted
inserted
replaced
654 |
654 |
655 datatype target_source = Literal of string | File of Path.T |
655 datatype target_source = Literal of string | File of Path.T |
656 |
656 |
657 local |
657 local |
658 |
658 |
659 val format_source = Pretty.block0 o Pretty.fbreaks o map Code_Printer.str o split_lines; |
659 val format_source = Pretty.block0 o Pretty.fbreaks o map Pretty.str o split_lines; |
660 |
660 |
661 fun eval_source (Literal s) = s |
661 fun eval_source (Literal s) = s |
662 | eval_source (File p) = File.read p; |
662 | eval_source (File p) = File.read p; |
663 |
663 |
664 fun arrange_printings prep_syms prep_source ctxt = |
664 fun arrange_printings prep_syms prep_source ctxt = |