# 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 \prolog.ML\ +declare [[show_main_goal]] + method_setup ptac = \Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\ "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>\show_main_goal\ true; - structure Prolog = struct