equal
deleted
inserted
replaced
606 |
606 |
607 |
607 |
608 (*** diagnostic commands and interfaces ***) |
608 (*** diagnostic commands and interfaces ***) |
609 |
609 |
610 fun print_locales thy = |
610 fun print_locales thy = |
611 Pretty.strs ("locales:" :: |
611 Pretty.block |
612 map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy))) |
612 (Pretty.breaks |
|
613 (Pretty.str "locales:" :: |
|
614 map (Pretty.mark_str o #1) |
|
615 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))) |
613 |> Pretty.writeln; |
616 |> Pretty.writeln; |
614 |
617 |
615 fun pretty_locale thy show_facts name = |
618 fun pretty_locale thy show_facts name = |
616 let |
619 let |
617 val ctxt = init name thy; |
620 val ctxt = init name thy; |