equal
deleted
inserted
replaced
82 |
82 |
83 (* preferences of Pure *) |
83 (* preferences of Pure *) |
84 |
84 |
85 val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => |
85 val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => |
86 let |
86 let |
87 fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); |
87 fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ()); |
88 fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); |
88 fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); |
89 in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) (); |
89 in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) (); |
90 |
90 |
91 val parallel_proof_pref = |
91 val parallel_proof_pref = |
92 let |
92 let |