Support Isabelle2021-1 without patches:

in the next release it will be simpler again.

NOTES.thy

@@ -115,28 +115,9 @@ text \<open>
   limited to commands that do not change the semantic state: see
   \<^ML>\<open>Toplevel.present\<close> and \<^ML>\<open>Toplevel.present_local_theory\<close>.
 
-  There is an adhoc change to support \<^verbatim>\<open>Toplevel.present_theory\<close> in
-  \<^file>\<open>$ISABELLE_DOF_HOME/src/patches/present_theory\<close>.
-
-  An alternative, without patching Isabelle2021-1 in production, is to use
-  the presentation hook together with a function like this:
-\<close>
-
-ML \<open>
-  fun present_segment pr (segment: Document_Output.segment) =
-    (case #span segment of
-      Command_Span.Span (Command_Span.Command_Span (name, _), toks) =>
-        let
-          val {span, command = tr, prev_state = st, state = st'} = segment;
-          val tr' =
-            Toplevel.empty
-            |> Toplevel.name (Toplevel.name_of tr)
-            |> Toplevel.position (Toplevel.pos_of tr)
-            |> Toplevel.present (pr name toks);
-          val st'' = Toplevel.command_exception false tr' st'
-            handle Runtime.EXCURSION_FAIL (exn, _) => Exn.reraise exn;
-        in {span = span, command = tr, prev_state = st, state = st''} end
-    | _ => segment);
+  Since \<^verbatim>\<open>Toplevel.present_theory\<close> is missing in Isabelle2021-1, we use a
+  workaround with an alternative presentation hook: it exports
+  \<^verbatim>\<open>document/latex_dof\<close> files instead of regular \<^verbatim>\<open>document/latex_dof\<close>.
 \<close>
 
 

src/DOF/Isa_DOF.thy

@@ -1628,13 +1628,91 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
       in [XML.Elem (m (Latex.output_name name), xml)] end;
   in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
 
+
+(* document output commands *)
+
+local
+
+(* alternative presentation hook (workaround for missing Toplevel.present_theory) *)
+
+structure Document_Commands = Theory_Data
+(
+  type T = (string * (meta_args_t -> Input.source -> Proof.context -> Latex.text)) list;
+  val empty = [];
+  val merge = AList.merge (op =) (K true);
+);
+
+fun get_document_command thy name =
+  AList.lookup (op =) (Document_Commands.get thy) name;
+
+fun document_segment (segment: Document_Output.segment) =
+  (case #span segment of
+    Command_Span.Span (Command_Span.Command_Span (name, _), _) =>
+      (case try Toplevel.theory_of (#state segment) of
+        SOME thy => get_document_command thy name
+      | _ => NONE)
+  | _ => NONE);
+
+fun present_segment (segment: Document_Output.segment) =
+  (case document_segment segment of
+    SOME pr =>
+      let
+        val {span, command = tr, prev_state = st, state = st'} = segment;
+        val src = Command_Span.content (#span segment) |> filter_out Document_Source.is_improper;
+        val parse = attributes -- Parse.document_source;
+        fun present ctxt =
+          let val (meta_args, text) = #1 (Token.syntax (Scan.lift parse) src ctxt);
+          in pr meta_args text ctxt end;
+        val tr' =
+          Toplevel.empty
+          |> Toplevel.name (Toplevel.name_of tr)
+          |> Toplevel.position (Toplevel.pos_of tr)
+          |> Toplevel.present (Toplevel.presentation_context #> present);
+        val st'' = Toplevel.command_exception false tr' st'
+          handle Runtime.EXCURSION_FAIL (exn, _) => Exn.reraise exn;
+        val FIXME =
+          Toplevel.setmp_thread_position tr (fn () =>
+            writeln ("present_segment" ^ Position.here (Toplevel.pos_of tr) ^ "\n" ^
+              XML.string_of (XML.Elem (Markup.empty, the_default [] (Toplevel.output_of st'))) ^ "\n---\n" ^
+              XML.string_of (XML.Elem (Markup.empty, the_default [] (Toplevel.output_of st''))))) ()
+      in {span = span, command = tr, prev_state = st, state = st''} end
+  | _ => segment);
+
+val _ =
+  Theory.setup (Thy_Info.add_presentation (fn {options, segments, ...} => fn thy =>
+    if exists (Toplevel.is_skipped_proof o #state) segments then ()
+    else
+      let
+        val segments' = map present_segment segments;
+        val body = Document_Output.present_thy options thy segments';
+      in
+        if Options.string options "document" = "false" orelse
+          forall (is_none o document_segment) segments' then ()
+        else
+          let
+            val thy_name = Context.theory_name thy;
+            val latex = Latex.isabelle_body thy_name body;
+          in Export.export thy \<^path_binding>\<open>document/latex_dof\<close> latex end
+      end));
+
+in
+
 fun document_command (name, pos) descr mark cmd =
-  Outer_Syntax.command (name, pos) descr
+  (Outer_Syntax.command (name, pos) descr
     (attributes -- Parse.document_source >>
       (fn (meta_args, text) =>
-        Toplevel.present_theory (cmd meta_args)
-        (Toplevel.presentation_context #> document_output_reports name mark meta_args text)));
+        Toplevel.theory (fn thy =>
+          let
+            val thy' = cmd meta_args thy;
+            val _ =
+              (case get_document_command thy' name of
+                SOME pr => ignore (pr meta_args text (Proof_Context.init_global thy'))
+              | NONE => ());
+          in thy' end)));
+   (Theory.setup o Document_Commands.map)
+     (AList.update (op =) (name, document_output_reports name mark)));
 
+end;
 
 
 (* Core Command Definitions *)

src/patches/present_theory

@@ -1,36 +0,0 @@
-# HG changeset patch
-# User wenzelm
-# Date 1639864289 -3600
-#      Sat Dec 18 22:51:29 2021 +0100
-# Node ID fcd643ddbfb2bcc60b301d8630d563ea265f7719
-# Parent  70be57333ea1b0e1866be2e944f2e0f70c437ae4
-Toplevel.present_theory for Isabelle/DOF;
-
-diff -r 70be57333ea1 -r fcd643ddbfb2 src/Pure/Isar/toplevel.ML
---- a/src/Pure/Isar/toplevel.ML	Sun Dec 12 10:42:51 2021 +0100
-+++ b/src/Pure/Isar/toplevel.ML	Sat Dec 18 22:51:29 2021 +0100
-@@ -55,6 +55,7 @@
-   val ignored: Position.T -> transition
-   val malformed: Position.T -> string -> transition
-   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
-+  val present_theory: (theory -> theory) -> (state -> Latex.text) -> transition -> transition
-   val theory': (bool -> theory -> theory) -> transition -> transition
-   val theory: (theory -> theory) -> transition -> transition
-   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
-@@ -452,6 +453,16 @@
-   (fn Theory gthy => node_presentation (Theory (f gthy))
-     | _ => raise UNDEF));
- 
-+fun present_theory f g = present_transaction (fn _ =>
-+  (fn Theory (Context.Theory thy) =>
-+      let val thy' = thy
-+        |> Sign.new_group
-+        |> f
-+        |> Sign.reset_group;
-+      in node_presentation (Theory (Context.Theory thy')) end
-+    | _ => raise UNDEF))
-+  (presentation g);
-+
- fun theory' f = transaction (fn int =>
-   (fn Theory (Context.Theory thy) =>
-       let val thy' = thy

src/scala/dof_document_build.scala

@@ -19,7 +19,21 @@ object DOF_Document_Build
       dir: Path,
       doc: Document_Build.Document_Variant): Document_Build.Directory =
     {
-      context.prepare_directory(dir, doc, new Latex_Output(context.options))
+      val latex_output = new Latex_Output(context.options)
+      val directory = context.prepare_directory(dir, doc, latex_output)
+
+      // produced by alternative presentation hook (workaround for missing Toplevel.present_theory)
+      for (name <- context.document_theories) {
+        val path = Path.basic(Document_Build.tex_name(name))
+        val xml =
+          YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text)
+        if (xml.nonEmpty) {
+          File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic))
+            .write(directory.doc_dir)
+        }
+      }
+
+      directory
     }
   }