Test with Isabelle 2023.

.woodpecker/build.yml

@@ -1,7 +1,9 @@
 pipeline:
   build:
-    image: docker.io/logicalhacking/isabelle2022
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
+    pull: true
     commands:
+      - hg log --limit 2 /root/isabelle
       - ./.woodpecker/check_dangling_theories
       - ./.woodpecker/check_external_file_refs
       - ./.woodpecker/check_quick_and_dirty
@@ -21,7 +23,7 @@ pipeline:
       - cd ../..
       - ln -s * latest
   archive:
-    image: docker.io/logicalhacking/isabelle2022
+    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle2023:latest
     commands:
       - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
       - mkdir -p $ARTIFACT_DIR

Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy

@@ -347,7 +347,7 @@ text\<open>
 \<^item> \<^ML>\<open>Context.proper_subthy : theory * theory -> bool\<close> subcontext test
 \<^item> \<^ML>\<open>Context.Proof: Proof.context -> Context.generic \<close> A constructor embedding local contexts
 \<^item> \<^ML>\<open>Context.proof_of : Context.generic -> Proof.context\<close> the inverse
-\<^item> \<^ML>\<open>Context.theory_name : theory -> string\<close>
+\<^item> \<^ML>\<open>Context.theory_name : {long:bool} -> theory -> string\<close>
 \<^item> \<^ML>\<open>Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic\<close>
 \<close>
 
@@ -358,7 +358,7 @@ text\<open>The structure \<^ML_structure>\<open>Proof_Context\<close> provides a
 \<^item> \<^ML>\<open>  Context.Proof: Proof.context -> Context.generic \<close>
   the path to a generic Context, i.e. a sum-type of global and local contexts
   in order to simplify system interfaces
-\<^item> \<^ML>\<open> Proof_Context.get_global: theory -> string -> Proof.context\<close>
+\<^item> \<^ML>\<open> Proof_Context.get_global: {long:bool} -> theory -> string -> Proof.context\<close>
 \<close>
 
 
@@ -886,7 +886,6 @@ datatype thy = Thy of
 \<^item>  \<^ML>\<open>Theory.axiom_space: theory -> Name_Space.T\<close>
 \<^item>  \<^ML>\<open>Theory.all_axioms_of: theory -> (string * term) list\<close>
 \<^item>  \<^ML>\<open>Theory.defs_of: theory -> Defs.T\<close>
-\<^item>  \<^ML>\<open>Theory.join_theory: theory list -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.at_begin: (theory -> theory option) -> theory -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.at_end: (theory -> theory option) -> theory -> theory\<close>
 \<^item>  \<^ML>\<open>Theory.begin_theory: string * Position.T -> theory list -> theory\<close>
@@ -1139,8 +1138,7 @@ text\<open>
    necessary infrastructure ---  i.e. the operations to pack and unpack theories and
    queries  on it:
 
-\<^item> \<^ML>\<open> Toplevel.theory_toplevel: theory -> Toplevel.state\<close>
-\<^item> \<^ML>\<open> Toplevel.init_toplevel: unit -> Toplevel.state\<close>
+\<^item> \<^ML>\<open> Toplevel.make_state: theory option -> Toplevel.state\<close>
 \<^item> \<^ML>\<open> Toplevel.is_toplevel: Toplevel.state -> bool\<close>
 \<^item> \<^ML>\<open> Toplevel.is_theory: Toplevel.state -> bool\<close>
 \<^item> \<^ML>\<open> Toplevel.is_proof: Toplevel.state -> bool\<close>
@@ -1178,7 +1176,7 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
  \<^item> \<^ML>\<open>Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
    adjoins a theory transformer.
  \<^item> \<^ML>\<open>Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\<close>
- \<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\<close>
+ \<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation option -> Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
  \<^item> \<^ML>\<open>Toplevel.present_local_theory:  (xstring * Position.T) option ->
@@ -1196,7 +1194,6 @@ text\<open>
  \<^item>  \<^ML>\<open>Document.state : unit -> Document.state\<close>, giving the state as a "collection" of named
      nodes, each consisting of an editable list of commands, associated with asynchronous 
      execution process,
- \<^item>  \<^ML>\<open>Session.get_keywords : unit -> Keyword.keywords\<close>, this looks to be session global,
  \<^item>  \<^ML>\<open>Thy_Header.get_keywords : theory -> Keyword.keywords\<close> this looks to be just theory global.
 
 
@@ -1270,7 +1267,6 @@ subsection\<open>Miscellaneous\<close>
 
 text\<open>Here are a few queries relevant for the global config of the isar engine:\<close>
 ML\<open> Document.state();\<close>
-ML\<open> Session.get_keywords(); (* this looks to be  session global. *) \<close>
 ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
 
   
@@ -1877,18 +1873,17 @@ Common Stuff related to Inner Syntax Parsing
 \<^item>\<^ML>\<open>Args.internal_typ : typ parser\<close>
 \<^item>\<^ML>\<open>Args.internal_term: term parser\<close>
 \<^item>\<^ML>\<open>Args.internal_fact: thm list parser\<close>
-\<^item>\<^ML>\<open>Args.internal_attribute: (morphism -> attribute) parser\<close>
-\<^item>\<^ML>\<open>Args.internal_declaration: declaration parser\<close>
+\<^item>\<^ML>\<open>Args.internal_attribute: attribute Morphism.entity parser\<close>
 \<^item>\<^ML>\<open>Args.alt_name    : string parser\<close>
 \<^item>\<^ML>\<open>Args.liberal_name: string parser\<close>
 
 
-
 Common Isar Syntax
 \<^item>\<^ML>\<open>Args.named_source: (Token.T -> Token.src) -> Token.src parser\<close>
 \<^item>\<^ML>\<open>Args.named_typ   : (string -> typ) -> typ parser\<close>
 \<^item>\<^ML>\<open>Args.named_term : (string -> term) -> term parser\<close>
-\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\<close>
+\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> Morphism.declaration_entity) ->
+    Morphism.declaration_entity parser\<close>
 \<^item>\<^ML>\<open>Args.typ_abbrev  : typ context_parser\<close>
 \<^item>\<^ML>\<open>Args.typ: typ context_parser\<close>
 \<^item>\<^ML>\<open>Args.term: term context_parser\<close>
@@ -2148,7 +2143,7 @@ text\<open>
 \<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
 \<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
 \<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
-\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
+\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> Keyword.keywords -> string -> Document_Output.segment list -> Latex.text \<close>
 
 \<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text  -> Latex.text\<close>
 \<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text  -> Latex.text\<close>

Isabelle_DOF-Unit-Tests/TestKit.thy

@@ -37,14 +37,13 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark
                                      xstring_opt:(xstring * Position.T) option),
                                     toks_list:Input.source list) 
                                   : theory -> theory =
-  let  val toplvl = Toplevel.theory_toplevel
-       val ((binding,cid_pos), doc_attrs) = meta_args
+  let  val ((binding,cid_pos), doc_attrs) = meta_args
        val oid = Binding.name_of binding
        val oid' = if meta_args = ODL_Meta_Args_Parser.empty_meta_args
                   then "output"
                   else oid
        (* as side-effect, generates markup *)
-       fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy);
+       fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (Toplevel.make_state (SOME thy))
                                       val pos = Input.pos_of toks;
                                       val _ =   Context_Position.reports ctxt
                                                 [(pos, Markup.language_document (Input.is_delimited toks)),

Isabelle_DOF/scala/dof.scala

@@ -39,10 +39,10 @@ import isabelle._
 object DOF {
   /** parameters **/
 
-  val isabelle_version = "2022"
-  val isabelle_url = "https://isabelle.in.tum.de/website-Isabelle2022"
+  val isabelle_version = "2023"
+  val isabelle_url = "https://isabelle.in.tum.de/website-Isabelle2023" 
 
-  val afp_version = "afp-2022-10-27"
+  val afp_version = "afp-2023-09-13"
 
   // Isabelle/DOF version: "Unreleased" for development, semantic version for releases
   val version = "Unreleased"
@@ -55,7 +55,7 @@ object DOF {
   val generic_doi = "10.5281/zenodo.3370482"
 
   // Isabelle/DOF source repository
-  val url = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+  val url = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/Isabelle_dev"
 
   // Isabelle/DOF release artifacts
   val artifact_dir = "releases/Isabelle_DOF/Isabelle_DOF"

Isabelle_DOF/scala/dof_document_build.scala

@@ -42,7 +42,7 @@ object DOF_Document_Build
     def the_document_entry(context: Document_Build.Context, name: String): Export.Entry = {
       val entries =
         for {
-          node_name <- context.document_theories
+          node_name <- context.all_document_theories
           entry <- context.session_context.get(node_name.theory, name)
         } yield entry
 
@@ -60,11 +60,12 @@ object DOF_Document_Build
     override def prepare_directory(
       context: Document_Build.Context,
       dir: Path,
-      doc: Document_Build.Document_Variant): Document_Build.Directory =
+      doc: Document_Build.Document_Variant,
+      verbose: Boolean): Document_Build.Directory =
     {
       val options = DOF.options(context.options)
       val latex_output = new Latex_Output(options)
-      val directory = context.prepare_directory(dir, doc, latex_output)
+      val directory = context.prepare_directory(dir, doc, latex_output, verbose)
 
       val isabelle_dof_dir = context.session_context.sessions_structure(DOF.session).dir
 

Isabelle_DOF/thys/Isa_DOF.thy

@@ -2021,7 +2021,7 @@ fun print_term meta_args_opt (string_list, string) trans =
 let
   val pos = Toplevel.pos_of trans
 in meta_args_exec meta_args_opt
-   #> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy))
+   #> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.make_state (SOME thy)))
    |> (fn thy => Toplevel.theory thy trans)
 end
 
@@ -2037,7 +2037,7 @@ in trans
         (fn thy =>
            if Config.get_global thy disable_assert_evaluation
            then (meta_args_exec meta_args_opt
-                 #> tap (fn thy => print_item (prin t pos) (modes, t) (Toplevel.theory_toplevel thy)))
+                 #> tap (fn thy => print_item (prin t pos) (modes, t) (Toplevel.make_state (SOME thy))))
                 thy
            else value_cmd {assert=true} meta_args_opt name modes t pos thy) 
 end
@@ -2346,12 +2346,9 @@ fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_
 
 fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
   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 sem_attrs transform_attr meta_args text
-               #> SOME): Toplevel.state -> Latex.text option)) );
+  (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
+      Toplevel.theory' (fn _ => cmd meta_args)
+          (SOME (Toplevel.presentation_context #> document_output_reports name mark sem_attrs transform_attr meta_args text)))); 
 
 fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt =
  let
@@ -2363,9 +2360,9 @@ fun onto_macro_cmd_command (name, pos) descr cmd output_cmd =
   (ODL_Meta_Args_Parser.attributes -- Parse.document_source >>  
      (fn (meta_args, text) =>
           Toplevel.theory' (fn _ => cmd meta_args)
-             (Toplevel.presentation_context
-              #> onto_macro_cmd_output_reports output_cmd (meta_args, text)
-              #> SOME))) 
+             (SOME (Toplevel.presentation_context
+              #> onto_macro_cmd_output_reports output_cmd  (meta_args, text)
+              ))))
 
 
 (* Core Command Definitions *)
@@ -2700,7 +2697,8 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt
       |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
     val atts = more_atts @ map (prep_att lthy) raw_atts;
 
-    val pos = Position.thread_data ();
+    val print_cfg = {interactive = int, pos = Position.thread_data (), proof_state= false} 
+
     fun after_qed' results goal_ctxt' =
       let
         val results' =
@@ -2712,12 +2710,12 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Binding.is_empty_atts (name, atts) then
-            (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results print_cfg lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results print_cfg lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
 

README_DEVELOPMENT.md

@@ -5,9 +5,9 @@
 Isabelle/DOF has three major prerequisites:
 
 * **Isabelle:** Isabelle/DOF requires [Isabelle
-  2022](https://isabelle.in.tum.de/website-Isabelle2022/). Please download the
-  Isabelle 2022 distribution for your operating system from the [Isabelle
-  website](https://isabelle.in.tum.de/website-Isabelle2022/).
+  2023](https://isabelle.in.tum.de/website-Isabelle2023/). Please download the
+  Isabelle 2023 distribution for your operating system from the [Isabelle
+  website](https://isabelle.in.tum.de/website-Isabelle2023/).
 * **AFP:** Isabelle/DOF requires several entries from the [Archive of Formal Proofs
   (AFP)](https://www.isa-afp.org/).  
 * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least