equal
deleted
inserted
replaced
65 end |
65 end |
66 |
66 |
67 val thm_deps_pref = |
67 val thm_deps_pref = |
68 let |
68 let |
69 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) |
69 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) |
70 fun set s = if PgipTypes.read_pgipbool s then |
70 fun set s = NAMED_CRITICAL "print_mode" (fn () => |
71 change print_mode (insert (op =) thm_depsN) |
71 if PgipTypes.read_pgipbool s then |
72 else |
72 change print_mode (insert (op =) thm_depsN) |
73 change print_mode (remove (op =) thm_depsN) |
73 else |
|
74 change print_mode (remove (op =) thm_depsN)) |
74 in |
75 in |
75 mkpref get set PgipTypes.Pgipbool "theorem-dependencies" |
76 mkpref get set PgipTypes.Pgipbool "theorem-dependencies" |
76 "Track theorem dependencies within Proof General" |
77 "Track theorem dependencies within Proof General" |
77 end |
78 end |
78 |
79 |