--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,153 @@
+(* Title: Pure/ProofGeneral/preferences.ML
+ ID: $Id$
+ Author: David Aspinall and Markus Wenzel
+
+User preferences for Isabelle which are maintained by the interface.
+*)
+
+signature PREFERENCES =
+sig
+ type pgiptype = PgipTypes.pgiptype
+
+ type isa_preference = { name: string,
+ descr: string,
+ default: string,
+ pgiptype: pgiptype,
+ get: unit -> string,
+ set: string -> unit }
+
+ val preferences : (string * isa_preference list) list
+end
+
+structure Preferences : PREFERENCES =
+struct
+
+val thm_depsN = "thm_deps"; (* also in proof_general_pgip.ML: move to pgip_isabelle? *)
+
+type pgiptype = PgipTypes.pgiptype
+
+type isa_preference = { name: string,
+ descr: string,
+ default: string,
+ pgiptype: pgiptype,
+ get: unit -> string,
+ set: string -> unit }
+
+
+fun mkpref get set typ nm descr =
+ { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference
+
+fun mkpref_from_ref read write typ r nm descr =
+ mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr
+
+val int_pref =
+ mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
+ (PgipTypes.Pgipint (NONE, NONE))
+val nat_pref =
+ mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat
+
+val bool_pref =
+ mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool
+
+val proof_pref =
+ let
+ fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
+ fun set s = proofs := (if (PgipTypes.read_pgipbool s) then 1 else 2)
+ in
+ mkpref get set PgipTypes.Pgipbool "full-proofs"
+ "Record full proof objects internally"
+ end
+
+val thm_deps_pref =
+ let
+ fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN)
+ fun set s = if (PgipTypes.read_pgipbool s) then
+ change print_mode (insert (op =) thm_depsN)
+ else
+ change print_mode (remove (op =) thm_depsN)
+ in
+ mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
+ "Track theorem dependencies within Proof General"
+ end
+
+val print_depth_pref =
+ let
+ val pg_print_depth_val = ref 10
+ fun get () = PgipTypes.int_to_pgstring (! pg_print_depth_val)
+ fun setn n = (print_depth n; pg_print_depth_val := n)
+ val set = setn o PgipTypes.read_pgipnat
+ in
+ mkpref get set PgipTypes.Pgipbool "print-depth" "Setting for the ML print depth"
+ end
+
+
+val display_preferences =
+ [bool_pref show_types
+ "show-types"
+ "Include types in display of Isabelle terms",
+ bool_pref show_sorts
+ "show-sorts"
+ "Include sorts in display of Isabelle terms",
+ bool_pref show_consts
+ "show-consts"
+ "Show types of consts in Isabelle goal display",
+ bool_pref long_names
+ "long-names"
+ "Show fully qualified names in Isabelle terms",
+ bool_pref show_brackets
+ "show-brackets"
+ "Show full bracketing in Isabelle terms",
+ bool_pref Proof.show_main_goal
+ "show-main-goal"
+ "Show main goal in proof state display",
+ bool_pref Syntax.eta_contract
+ "eta-contract"
+ "Print terms eta-contracted"]
+
+val advanced_display_preferences =
+ [nat_pref goals_limit
+ "goals-limit"
+ "Setting for maximum number of goals printed",
+ int_pref ProofContext.prems_limit
+ "prems-limit"
+ "Setting for maximum number of premises printed",
+ print_depth_pref,
+ bool_pref show_question_marks
+ "show-question-marks"
+ "Show leading question mark of variable name"]
+
+val tracing_preferences =
+ [bool_pref trace_simp
+ "trace-simplifier"
+ "Trace simplification rules.",
+ nat_pref trace_simp_depth_limit
+ "trace-simplifier-depth"
+ "Trace simplifier depth limit.",
+ bool_pref trace_rules
+ "trace-rules"
+ "Trace application of the standard rules",
+ bool_pref Pattern.trace_unify_fail
+ "trace-unification"
+ "Output error diagnostics during unification",
+ bool_pref Output.timing
+ "global-timing"
+ "Whether to enable timing in Isabelle.",
+ bool_pref Output.show_debug_msgs
+ "debug-messages"
+ "Whether to show debugging messages."]
+
+val proof_preferences =
+ [bool_pref quick_and_dirty
+ "quick-and-dirty"
+ "Take a few short cuts",
+ bool_pref Toplevel.skip_proofs
+ "skip-proofs"
+ "Ignore proof scripts (interactive-only)"]
+
+val preferences =
+ [("Display", display_preferences),
+ ("Advanced Display", advanced_display_preferences),
+ ("Tracing", tracing_preferences),
+ ("Proof", proof_preferences)]
+
+end