diff --git a/NOTES.thy b/NOTES.thy index a689bd3c..f45aea38 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -80,6 +80,17 @@ text \ section \Document preparation in Isabelle/ML\ +subsection \Session presentation hook\ + +text \ + \<^ML>\Build.add_hook\ allows to install a global session presentation + hook. It is used e.g. in Isabelle/Mirabelle to analyze all loaded + theories via Sledgehammer and other tools. Isabelle/DOF could use it to + "wrap-up" the whole session, to check if all document constraints hold + (cf. "monitors"). +\ + + subsection \Theory presentation hook\ text \ @@ -129,6 +140,15 @@ ML \ \ +subsection \Document content\ + +text \ + XML is now used uniformly (sometimes as inlined YXML). The meaning of + markup elements and properties is defined in + \<^scala_type>\isabelle.Latex.Output\ (or user-defined subclasses). +\ + + section \Isabelle/Scala services\ subsection \Isabelle/DOF/Scala module\