equal
deleted
inserted
replaced
75 |
75 |
76 val _ = |
76 val _ = |
77 ProofGeneral.preference ProofGeneral.category_advanced_display |
77 ProofGeneral.preference ProofGeneral.category_advanced_display |
78 NONE |
78 NONE |
79 (Markup.print_int o get_default_print_depth) |
79 (Markup.print_int o get_default_print_depth) |
80 (put_default_print_depth o Markup.parse_int) |
80 (default_print_depth o Markup.parse_int) |
81 ProofGeneral.pgipint |
81 ProofGeneral.pgipint |
82 "print-depth" |
82 "print-depth" |
83 "Setting for the ML print depth"; |
83 "Setting for the ML print depth"; |
84 |
84 |
85 val _ = |
85 val _ = |