# HG changeset patch
# User wenzelm
# Date 1662667566 -7200
# Node ID 922e3f9251acebfabfd590a43158a3746fd2c106
# Parent  f8eff19a38257cbf5d048b430ed22e66434190c2
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);

diff -r f8eff19a3825 -r 922e3f9251ac src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Thu Sep 08 20:46:22 2022 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Thu Sep 08 22:06:06 2022 +0200
@@ -10,6 +10,8 @@
 
 ML_file \<open>prolog.ML\<close>
 
+declare [[show_main_goal]]
+
 method_setup ptac =
   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
   "basic Lambda Prolog interpreter"
diff -r f8eff19a3825 -r 922e3f9251ac src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Thu Sep 08 20:46:22 2022 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Sep 08 22:06:06 2022 +0200
@@ -2,8 +2,6 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-Options.default_put_bool \<^system_option>\<open>show_main_goal\<close> true;
-
 structure Prolog =
 struct