# HG changeset patch # User wenzelm # Date 1223990172 -7200 # Node ID 52ec4c827ed4a8ed0a3316f95192c05c10b3ee64 # Parent d238b83ba3fcbe7011ad97ac190c94cc14a38fc6 export generic_pref etc.; CRITICAL access to preferences; misc cleanup, more conventional indentation; diff -r d238b83ba3fc -r 52ec4c827ed4 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Tue Oct 14 15:16:11 2008 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Tue Oct 14 15:16:12 2008 +0200 @@ -7,191 +7,194 @@ signature PREFERENCES = sig - type pgiptype = PgipTypes.pgiptype - - type isa_preference = { name: string, - descr: string, - default: string, - pgiptype: pgiptype, - get: unit -> string, - set: string -> unit } - - (* table of categories and preferences; names must be unique *) - type isa_preference_table = (string * isa_preference list) list - - val preferences : isa_preference_table - - val remove : string -> isa_preference_table -> isa_preference_table - val add : string -> isa_preference - -> isa_preference_table -> isa_preference_table - val set_default : string * string -> isa_preference_table -> isa_preference_table + type preference = + {name: string, + descr: string, + default: string, + pgiptype: PgipTypes.pgiptype, + get: unit -> string, + set: string -> unit} + val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype -> + 'a ref -> string -> string -> preference + val string_pref: string ref -> string -> string -> preference + val int_pref: int ref -> string -> string -> preference + val nat_pref: int ref -> string -> string -> preference + val bool_pref: bool ref -> string -> string -> preference + type T = (string * preference list) list + val pure_preferences: T + val remove: string -> T -> T + val add: string -> preference -> T -> T + val set_default: string * string -> T -> T end -structure Preferences : PREFERENCES = +structure Preferences: PREFERENCES = struct -val thm_depsN = "thm_deps"; (* also in proof_general_pgip.ML: move to pgip_isabelle? *) - -type pgiptype = PgipTypes.pgiptype +(* preferences and preference tables *) -type isa_preference = { name: string, - descr: string, - default: string, - pgiptype: pgiptype, - get: unit -> string, - set: string -> unit } +type preference = + {name: string, + descr: string, + default: string, + pgiptype: PgipTypes.pgiptype, + get: unit -> string, + set: string -> unit}; + +fun mkpref raw_get raw_set typ name descr : preference = + let + fun get () = CRITICAL raw_get; + fun set x = CRITICAL (fn () => raw_set x); + in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end; -fun mkpref get set typ nm descr = - { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference +(* generic preferences *) -fun mkpref_from_ref read write typ r nm descr = - mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr +fun generic_pref read write typ r = + mkpref (fn () => read (! r)) (fn x => r := write x) typ; + +val string_pref = generic_pref I I PgipTypes.Pgipstring; val int_pref = - mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE)) - (PgipTypes.Pgipint (NONE, NONE)) + generic_pref 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 + generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat; val bool_pref = - mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool + generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool; + + +(* preferences of Pure *) val proof_pref = - let - fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2) - fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1) - in - mkpref get set PgipTypes.Pgipbool "full-proofs" - "Record full proof objects internally" - end + let + fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); + fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); + in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end; +val thm_depsN = "thm_deps"; val thm_deps_pref = - let - fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) - fun set s = NAMED_CRITICAL "print_mode" (fn () => - 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 + let + fun get () = PgipTypes.bool_to_pgstring (print_mode_active 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 - fun get () = PgipTypes.int_to_pgstring (get_print_depth ()) - val set = print_depth o PgipTypes.read_pgipnat - in - mkpref get set PgipTypes.Pgipnat - "print-depth" "Setting for the ML print depth" - end + let + fun get () = PgipTypes.int_to_pgstring (get_print_depth ()); + val set = print_depth o PgipTypes.read_pgipnat; + in mkpref get set PgipTypes.Pgipnat "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"] + [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"] + [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 Toplevel.debug - "debugging" - "Whether to enable debugging.", - bool_pref Quickcheck.auto - "auto-quickcheck" - "Whether to enable quickcheck automatically.", - nat_pref Quickcheck.auto_time_limit - "auto-quickcheck-time-limit" - "Time limit for automatic quickcheck (in milliseconds).", - thm_deps_pref] + [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 Toplevel.debug + "debugging" + "Whether to enable debugging.", + bool_pref Quickcheck.auto + "auto-quickcheck" + "Whether to enable quickcheck automatically.", + nat_pref Quickcheck.auto_time_limit + "auto-quickcheck-time-limit" + "Time limit for automatic quickcheck (in milliseconds).", + thm_deps_pref]; val proof_preferences = - [bool_pref quick_and_dirty - "quick-and-dirty" - "Take a few short cuts", - bool_pref Toplevel.skip_proofs - "skip-proofs" - "Skip over proofs (interactive-only)", - proof_pref, - nat_pref Multithreading.max_threads - "max-threads" - "Maximum number of threads"] + [bool_pref quick_and_dirty + "quick-and-dirty" + "Take a few short cuts", + bool_pref Toplevel.skip_proofs + "skip-proofs" + "Skip over proofs (interactive-only)", + proof_pref, + nat_pref Multithreading.max_threads + "max-threads" + "Maximum number of threads"]; -val preferences = - [("Display", display_preferences), - ("Advanced Display", advanced_display_preferences), - ("Tracing", tracing_preferences), - ("Proof", proof_preferences)] +val pure_preferences = + [("Display", display_preferences), + ("Advanced Display", advanced_display_preferences), + ("Tracing", tracing_preferences), + ("Proof", proof_preferences)]; -type isa_preference_table = (string * isa_preference list) list + +(* table of categories and preferences; names must be unique *) + +type T = (string * preference list) list; -fun remove name (preftable : isa_preference_table) = - map (fn (cat,prefs) => - (cat, filter_out (curry op= name o #name) prefs)) - preftable; +fun remove name (tab: T) = tab |> map + (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs)); -fun set_default (setname,newdefault) (preftable : isa_preference_table) = - map (fn (cat,prefs) => - (cat, map (fn (pref as {name,descr,default,pgiptype,get,set}) - => if (name = setname) then - (set newdefault; - {name=name,descr=descr,default=newdefault, - pgiptype=pgiptype,get=get,set=set}) - else pref) - prefs)) - preftable; +fun set_default (setname, newdefault) (tab: T) = tab |> map + (fn (cat, prefs) => + (cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) => + if name = setname then + (set newdefault; + {name =name , descr = descr, default = newdefault, + pgiptype = pgiptype, get = get, set = set}) + else pref))); -fun add cname (pref: isa_preference) (preftable : isa_preference_table) = - map (fn (cat,prefs:isa_preference list) => - if cat <> cname then (cat,prefs) - else if (#name pref) mem (map #name prefs) - then error ("Preference already exists: " ^ quote(#name pref)) - else (cat, pref::prefs)) preftable; +fun add cname (pref: preference) (tab: T) = tab |> map + (fn (cat, prefs) => + if cat <> cname then (cat, prefs) + else + if exists (fn {name, ...} => name = #name pref) prefs + then error ("Preference already exists: " ^ quote (#name pref)) + else (cat, pref :: prefs)); -end +end;