author wenzelm
Tue, 31 Jul 2007 21:19:22 +0200
changeset 24100 a2f19514e156
parent 22587 5454b06320fb
child 24191 333f0a4bcc55
permissions -rw-r--r--
added max-threads preference;

(*  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 = 
  type pgiptype = PgipTypes.pgiptype

  type isa_preference = { name: string,
			  descr: string,
			  default: string,
			  pgiptype: pgiptype,
			  get: unit -> string,
			  set: string -> unit }

  (* table of categorised 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 set_default : string * string -> isa_preference_table -> isa_preference_table

structure Preferences : PREFERENCES =

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 =
	fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
	fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
	mkpref get set PgipTypes.Pgipbool "full-proofs" 
	       "Record full proof objects internally"

val thm_deps_pref = 
	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)
			change print_mode (remove (op =) thm_depsN) 
	mkpref get set PgipTypes.Pgipbool "theorem-dependencies" 
	       "Track theorem dependencies within Proof General"

val print_depth_pref =
	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
	mkpref get set PgipTypes.Pgipnat
	       "print-depth" "Setting for the ML print depth"

val display_preferences = 
    [bool_pref show_types
	       "Include types in display of Isabelle terms",
     bool_pref show_sorts
	       "Include sorts in display of Isabelle terms",
     bool_pref show_consts
	       "Show types of consts in Isabelle goal display",
     bool_pref long_names
	       "Show fully qualified names in Isabelle terms",
     bool_pref show_brackets
	       "Show full bracketing in Isabelle terms",
     bool_pref Proof.show_main_goal
	       "Show main goal in proof state display",
     bool_pref Syntax.eta_contract
	       "Print terms eta-contracted"]

val advanced_display_preferences =
    [nat_pref goals_limit
	      "Setting for maximum number of goals printed",
     int_pref ProofContext.prems_limit
	      "Setting for maximum number of premises printed",
     bool_pref show_question_marks
	       "Show leading question mark of variable name"]

val tracing_preferences = 
    [bool_pref trace_simp
	       "Trace simplification rules.",
     nat_pref trace_simp_depth_limit
	      "Trace simplifier depth limit.",
     bool_pref trace_rules
	       "Trace application of the standard rules",
     bool_pref Pattern.trace_unify_fail
	       "Output error diagnostics during unification",
     bool_pref Output.timing
	       "Whether to enable timing in Isabelle.",
     bool_pref Toplevel.debug
		"Whether to enable debugging."]

val proof_preferences = 
    [bool_pref quick_and_dirty
	       "Take a few short cuts",
     bool_pref Toplevel.skip_proofs
	       "Skip over proofs (interactive-only)",
     nat_pref Multithreading.max_threads
	       "Maximum number of threads"]

val preferences = 
    [("Display", display_preferences),
     ("Advanced Display", advanced_display_preferences),
     ("Tracing", tracing_preferences),
     ("Proof", proof_preferences)]

type isa_preference_table = (string * isa_preference list) list

fun remove name (preftable : isa_preference_table)  = 
    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;
			     else pref)