added settings: eta-contract, goals-limit, prems-limit;

1 files changed, 15 insertions, 0 deletions

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index dc4bf761..5bbc5df1 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -285,6 +285,11 @@ until Proof General is restarted."
   :type 'boolean
   :setting "long_names:=%b;")
 
+(defpacustom eta-contract  t
+  "Whether to print terms eta-contracted in Isabelle."
+  :type 'boolean
+  :setting "Syntax.eta_contract:=%b;")
+
 (defpacustom trace-simplifier  nil
   "Whether to trace the Simplifier in Isabelle."
   :type 'boolean
@@ -300,6 +305,16 @@ until Proof General is restarted."
   :type 'boolean
   :setting "Library.timing:=%b;")
 
+(defpacustom goals-limit  10
+  "Setting for maximum number of goals printed in Isabelle."
+  :type 'integer
+  :setting "goals_limit:=%i;")
+
+(defpacustom prems-limit  10
+  "Setting for maximum number of premises printed in Isabelle/Isar."
+  :type 'integer
+  :setting "ProofContext.prems_limit:=%i;")
+
 (defpacustom print-depth  10
   "Setting for the ML print depth in Isabelle."
   :type 'integer