Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
authorwenzelm
Thu, 08 Sep 2022 22:06:06 +0200
changeset 76091 922e3f9251ac
parent 76090 f8eff19a3825
child 76092 282f5e980a67
proper context option: change of underlying Options.default will not survive PIDE "Prover.options" (e.g. change of Isabelle/jEdit plugin options);
src/HOL/Prolog/HOHH.thy file | annotate | diff | comparison | revisions
src/HOL/Prolog/prolog.ML file | annotate | diff | comparison | revisions 
--- 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"
--- 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
isabelle