From ac4cc90efcfdd6335dd80339eedead6c6c6c5552 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Mon, 2 Oct 2000 23:22:30 +0000
Subject: added settings: eta-contract, goals-limit, prems-limit;

---
 isa/isabelle-system.el | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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
-- 
cgit v1.2.3