equal
deleted
inserted
replaced
48 val print_configs: Toplevel.transition -> Toplevel.transition |
48 val print_configs: Toplevel.transition -> Toplevel.transition |
49 val print_theorems: bool -> Toplevel.transition -> Toplevel.transition |
49 val print_theorems: bool -> Toplevel.transition -> Toplevel.transition |
50 val print_locales: Toplevel.transition -> Toplevel.transition |
50 val print_locales: Toplevel.transition -> Toplevel.transition |
51 val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition |
51 val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition |
52 val print_registrations: string -> Toplevel.transition -> Toplevel.transition |
52 val print_registrations: string -> Toplevel.transition -> Toplevel.transition |
|
53 val print_dependencies: bool * Expression.expression -> Toplevel.transition |
|
54 -> Toplevel.transition |
53 val print_attributes: Toplevel.transition -> Toplevel.transition |
55 val print_attributes: Toplevel.transition -> Toplevel.transition |
54 val print_simpset: Toplevel.transition -> Toplevel.transition |
56 val print_simpset: Toplevel.transition -> Toplevel.transition |
55 val print_rules: Toplevel.transition -> Toplevel.transition |
57 val print_rules: Toplevel.transition -> Toplevel.transition |
56 val print_trans_rules: Toplevel.transition -> Toplevel.transition |
58 val print_trans_rules: Toplevel.transition -> Toplevel.transition |
57 val print_methods: Toplevel.transition -> Toplevel.transition |
59 val print_methods: Toplevel.transition -> Toplevel.transition |
340 |
342 |
341 fun print_registrations name = Toplevel.unknown_context o |
343 fun print_registrations name = Toplevel.unknown_context o |
342 Toplevel.keep (fn state => |
344 Toplevel.keep (fn state => |
343 Locale.print_registrations (Toplevel.context_of state) name); |
345 Locale.print_registrations (Toplevel.context_of state) name); |
344 |
346 |
|
347 fun print_dependencies (clean, expression) = Toplevel.unknown_context o |
|
348 Toplevel.keep (fn state => |
|
349 Expression.print_dependencies (Toplevel.context_of state) clean expression); |
|
350 |
345 val print_attributes = Toplevel.unknown_theory o |
351 val print_attributes = Toplevel.unknown_theory o |
346 Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); |
352 Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); |
347 |
353 |
348 val print_simpset = Toplevel.unknown_context o |
354 val print_simpset = Toplevel.unknown_context o |
349 Toplevel.keep (fn state => |
355 Toplevel.keep (fn state => |