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 =>