From f44f0af01c7e11a18dfdfa93b009476945c70384 Mon Sep 17 00:00:00 2001 From: Makarius Date: Thu, 1 Dec 2022 22:48:45 +0100 Subject: [PATCH] Use regular Toplevel.presentation from Isabelle2022, without alternative presentation hook --- src/DOF/Isa_DOF.thy | 100 ++--------------------------- src/scala/dof_document_build.scala | 10 --- src/tests/Isabelle2021-1.thy | 7 +- 3 files changed, 5 insertions(+), 112 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 3d2c88fc..23927c03 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -2042,103 +2042,11 @@ fun document_output_reports name {markdown, body} meta_args text ctxt = (* document output commands *) -local - -(* alternative presentation hook (workaround for missing Toplevel.present_theory) *) - -structure Document_Commands = Theory_Data -( - type T = (string * (ODL_Meta_Args_Parser.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 = ODL_Meta_Args_Parser.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>\document/latex_dof\ latex end - end)); - -in - fun document_command (name, pos) descr mark cmd = - (Outer_Syntax.command (name, pos) descr - (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> - (fn (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))); - -fun document_command' (name, pos) descr mark = - (Outer_Syntax.command (name, pos) descr - (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> - (fn (meta_args, text) => - Toplevel.theory (fn thy => - let - 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; + Outer_Syntax.command (name, pos) descr + (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) => + Toplevel.theory' (fn _ => cmd meta_args) + (Toplevel.presentation_context #> document_output_reports name mark meta_args text #> SOME))); (* Core Command Definitions *) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 7fdc9850..3275bb27 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -48,16 +48,6 @@ object DOF_Document_Build val latex_output = new Latex_Output(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.iterator - entry <- context.session_context.get(name.theory, Export.DOCUMENT_LATEX + "_dof") - } { - val path = Path.basic(Document_Build.tex_name(name)) - val xml = YXML.parse_body(entry.text) - File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) - .write(directory.doc_dir) - } val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir // copy Isabelle/DOF LaTeX templates diff --git a/src/tests/Isabelle2021-1.thy b/src/tests/Isabelle2021-1.thy index 6a8759db..b9f000d5 100644 --- a/src/tests/Isabelle2021-1.thy +++ b/src/tests/Isabelle2021-1.thy @@ -107,13 +107,8 @@ subsection \Document commands\ text \ Isar toplevel commands now support a uniform concept for - \<^ML_type>\Toplevel.presentation\, but the exported interfaces are - limited to commands that do not change the semantic state: see + \<^ML_type>\Toplevel.presentation\, e.g. see \<^ML>\Toplevel.present\ and \<^ML>\Toplevel.present_local_theory\. - - Since \<^verbatim>\Toplevel.present_theory\ is missing in Isabelle2021-1, we use a - workaround with an alternative presentation hook: it exports - \<^verbatim>\document/latex_dof\ files instead of regular \<^verbatim>\document/latex_dof\. \