Use regular Toplevel.presentation from Isabelle2022, without alternative presentation hook

This commit is contained in:
Makarius Wenzel 2022-12-01 22:48:45 +01:00
parent 9a11baf840
commit f44f0af01c
3 changed files with 5 additions and 112 deletions

View File

@ -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>\<open>document/latex_dof\<close> 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 *)

View File

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

View File

@ -107,13 +107,8 @@ subsection \<open>Document commands\<close>
text \<open>
Isar toplevel commands now support a uniform concept for
\<^ML_type>\<open>Toplevel.presentation\<close>, but the exported interfaces are
limited to commands that do not change the semantic state: see
\<^ML_type>\<open>Toplevel.presentation\<close>, e.g. see
\<^ML>\<open>Toplevel.present\<close> and \<^ML>\<open>Toplevel.present_local_theory\<close>.
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>