From 0c8a0e1d63eef778a5df8e4363d9d6e0df25213a Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:30:49 +0200 Subject: [PATCH] Adapted to Isabelle/1ac2416e8432 -- approx. Isabelle2022 release. --- .../TR_MyCommentedIsabelle.thy | 12 ++++-------- src/DOF/Isa_COL.thy | 2 +- src/DOF/Isa_DOF.thy | 8 ++++---- src/DOF/RegExpInterface.thy | 2 +- src/scala/dof_document_build.scala | 14 +++++++------- src/tests/OutOfOrderPresntn.thy | 6 +++--- 6 files changed, 20 insertions(+), 24 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index bf6510d..e892b5e 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1183,7 +1183,7 @@ text\ The extensibility of Isabelle as a system framework depends on a num \<^item> \<^ML>\Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\ adjoins a theory transformer. \<^item> \<^ML>\Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\ - \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.exit: Toplevel.transition -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.ignored: Position.T -> Toplevel.transition\ \<^item> \<^ML>\Toplevel.present_local_theory: (xstring * Position.T) option -> @@ -1865,12 +1865,11 @@ Common Isar Syntax \<^item>\<^ML>\Args.name_position: (string * Position.T) parser\ \<^item>\<^ML>\Args.cartouche_inner_syntax: string parser\ \<^item>\<^ML>\Args.cartouche_input: Input.source parser\ -\<^item>\<^ML>\Args.text_token: Token.T parser \ Common Isar Syntax -\<^item>\<^ML>\Args.text_input: Input.source parser\ -\<^item>\<^ML>\Args.text : string parser\ +\<^item>\<^ML>\Parse.embedded_input: Input.source parser\ +\<^item>\<^ML>\Parse.embedded : string parser\ \<^item>\<^ML>\Args.binding : Binding.binding parser\ Common Stuff related to Inner Syntax Parsing @@ -1893,8 +1892,7 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term : (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ +\<^item>\<^ML>\Args.embedded_declaration: (Input.source -> declaration) -> declaration parser\ \<^item>\<^ML>\Args.typ_abbrev : typ context_parser\ \<^item>\<^ML>\Args.typ: typ context_parser\ \<^item>\<^ML>\Args.term: term context_parser\ @@ -1903,8 +1901,6 @@ Common Isar Syntax \<^item>\<^ML>\Args.named_source: (Token.T -> Token.src) -> Token.src parser\ \<^item>\<^ML>\Args.named_typ : (string -> typ) -> typ parser\ \<^item>\<^ML>\Args.named_term: (string -> term) -> term parser\ -\<^item>\<^ML>\Args.text_declaration: (Input.source -> declaration) -> declaration parser\ -\<^item>\<^ML>\Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\ Syntax for some major Pure commands in Isar \<^item>\<^ML>\Args.prop: term context_parser\ diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 409269a..9440515 100644 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -206,7 +206,7 @@ fun check_latex_measure _ src = handle Fail _ => error ("syntax error in LaTeX measure") ) in () end -val parse_latex_measure = Args.text_input >> (fn src => (check_latex_measure () (* dummy arg *) src; +val parse_latex_measure = Parse.embedded_input >> (fn src => (check_latex_measure () (* dummy arg *) src; (fst o Input.source_content) src ) ) end\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 1164ebf..b2047c1 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -2364,7 +2364,7 @@ val docitem_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc {unchecked = false, define= false} (* default *); -val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)) +val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_input)) : ({define:bool,unchecked:bool} * Input.source) context_parser; @@ -2835,7 +2835,7 @@ fun string_2_theory_text_antiquotation ctxt text = end fun gen_text_antiquotation name reportNcheck compile = - Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -2848,7 +2848,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) = (* should be the same as (2020): fun text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val _ = report_text ctxt text; @@ -2864,7 +2864,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms (* should be the same as (2020): fun theory_text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt; diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy index 81c81f7..873ac27 100644 --- a/src/DOF/RegExpInterface.thy +++ b/src/DOF/RegExpInterface.thy @@ -118,7 +118,7 @@ ML\ fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f)) val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args) val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files)) - val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files + val ml_content = map (fn f => Syntax.read_input (Bytes.content (#content f))) ml_files fun eval ml_content = fold (fn sml => (ML_Context.exec (fn () => ML_Context.eval_source ML_Compiler.flags sml))) ml_content diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index be9ba11..22fd697 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -50,14 +50,14 @@ object DOF_Document_Build 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) { + 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(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) - } + val xml = YXML.parse_body(entry.text) + File.content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) + .write(directory.doc_dir) } val dof_home= Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); // print(context.options.string("dof_url")); diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index fd8207e..dc37733 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -244,7 +244,7 @@ fun string_2_theory_text_antiquotation ctxt text = end fun gen_text_antiquotation name reportNcheck compile = - Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -257,7 +257,7 @@ fun std_text_antiquotation name (* redefined in these more abstract terms *) = (* should be the same as (2020): fun text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val _ = report_text ctxt text; @@ -273,7 +273,7 @@ fun std_theory_text_antiquotation name (* redefined in these more abstract terms (* should be the same as (2020): fun theory_text_antiquotation name = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt;