From 81c1d54f9b89d6d201f786ae3c8d8b85e6f73749 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Thu, 5 Oct 2023 15:28:15 +0200 Subject: [PATCH] Update build to Isabelle 2023 --- .github/workflows/pages.yml | 3 ++- ExportInfo.thy | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 2ddffe7..a50e618 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -18,7 +18,8 @@ jobs: mkdir AOT.ExportInfo chmod 777 output chmod 777 AOT.ExportInfo - docker run -v "$(pwd):/home/isabelle/AOT:rw" makarius/isabelle:Isabelle2021-1 build -D /home/isabelle/AOT -o browser_info -P /home/isabelle/AOT/output -e + sed -i -e 's/document = pdf, //' ROOT + docker run -v "$(pwd):/home/isabelle/AOT:rw" makarius/isabelle:Isabelle2023 build -D /home/isabelle/AOT -o browser_info -P /home/isabelle/AOT/output -e cp -r output build - name: Patch pages. run: .github/workflows/patch_pages.py build/Unsorted/AOT/*.html diff --git a/ExportInfo.thy b/ExportInfo.thy index 64eb34c..b115616 100644 --- a/ExportInfo.thy +++ b/ExportInfo.thy @@ -27,7 +27,7 @@ val global_facts = Global_Theory.facts_of thy; in Facts.dest_all (Context.Proof ctxt) false [] global_facts |> map (fn (n, thms) => let - val {concealed = _, group = _, theory_long_name = thy_name, pos = pos, serial = _} = + val {theory_long_name = thy_name, pos = pos, ...} = Name_Space.the_entry (Facts.space_of global_facts) n val name = Binding.name_of (Binding.qualified_name n) val items = Symtab.keys (fold (fn thm => fn set =>