From 0c8a0e1d63eef778a5df8e4363d9d6e0df25213a Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:30:49 +0200 Subject: [PATCH 1/4] 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; From 15feeb7d92a946da245c8c42bfbc007e52da2c5e Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:38:01 +0200 Subject: [PATCH 2/4] More standard package name: appears to work properly in Isabelle2022. --- etc/build.props | 4 ++-- src/scala/dof_document_build.scala | 2 +- src/scala/dof_mkroot.scala | 2 +- src/scala/dof_tools.scala | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/etc/build.props b/etc/build.props index af46f5e..dc6522d 100644 --- a/etc/build.props +++ b/etc/build.props @@ -8,5 +8,5 @@ sources = \ src/scala/dof_mkroot.scala \ src/scala/dof_tools.scala services = \ - isabelle_dof.DOF_Tools \ - isabelle_dof.DOF_Document_Build$Engine + isabelle.dof.DOF_Tools \ + isabelle.dof.DOF_Document_Build$Engine diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 22fd697..19b2a11 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -28,7 +28,7 @@ * SPDX-License-Identifier: BSD-2-Clause */ -package isabelle_dof +package isabelle.dof import isabelle._ import java.io.{File => JFile} diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala index d37419f..6cf160f 100644 --- a/src/scala/dof_mkroot.scala +++ b/src/scala/dof_mkroot.scala @@ -34,7 +34,7 @@ Prepare session root directory for Isabelle/DOF. */ -package isabelle_dof +package isabelle.dof import isabelle._ diff --git a/src/scala/dof_tools.scala b/src/scala/dof_tools.scala index b21fee3..b298a73 100644 --- a/src/scala/dof_tools.scala +++ b/src/scala/dof_tools.scala @@ -29,7 +29,7 @@ */ -package isabelle_dof +package isabelle.dof import isabelle._ From 5ac41a72ac0909c260f504292bd84b03fc8b8a53 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 21:58:10 +0200 Subject: [PATCH 3/4] More accurate treatment of sty files: do not just copy from all examples. --- src/scala/dof_document_build.scala | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 19b2a11..d70a10d 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -31,7 +31,6 @@ package isabelle.dof import isabelle._ -import java.io.{File => JFile} object DOF_Document_Build @@ -59,22 +58,22 @@ object DOF_Document_Build 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")); + val dof_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME")); // print(context.options.string("dof_url")); // copy Isabelle/DOF LaTeX templates - val template_dir = dof_home + Path.explode("src/document-templates/") + val template_dir = dof_home + Path.explode("src/document-templates") // TODO: error handling in case 1) template does not exist or 2) root.tex does already exist val template = regex.replaceAllIn(context.options.string("dof_template"),"") Isabelle_System.copy_file(template_dir + Path.explode("root-"+template+".tex"), directory.doc_dir+Path.explode("root.tex")) - // copy Isabelle/DOF LaTeX styles - val doc_jdir = new JFile(directory.doc_dir.implode) - val styles = File.find_files(new JFile(dof_home.implode),((f:JFile) => f.getName().endsWith(".sty")), true) - for (sty <- styles) { - Isabelle_System.copy_file(sty, doc_jdir) - } + // copy Isabelle/DOF LaTeX styles + List(Path.explode("src/DOF/latex"), Path.explode("src/ontologies")) + .flatMap(dir => + File.find_files((dof_home + dir).file, + file => file.getName.endsWith(".sty"), include_dirs = true)) + .foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file)) // create ontology.sty val ltx_styles = context.options.string("dof_ontologies").split(" +").map(s => regex.replaceAllIn(s,"")) From 516f5d2f79e94c2cffbaaac253820276f5a3f755 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 24 Oct 2022 22:11:30 +0200 Subject: [PATCH 4/4] Merely use session structure instead of component settings. --- src/scala/dof_document_build.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index d70a10d..31d8859 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -58,20 +58,20 @@ object DOF_Document_Build 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")); + val isabelle_dof_dir = context.session_context.sessions_structure("Isabelle_DOF").dir // print(context.options.string("dof_url")); // copy Isabelle/DOF LaTeX templates - val template_dir = dof_home + Path.explode("src/document-templates") + val template_dir = isabelle_dof_dir + Path.explode("document-templates") // TODO: error handling in case 1) template does not exist or 2) root.tex does already exist val template = regex.replaceAllIn(context.options.string("dof_template"),"") Isabelle_System.copy_file(template_dir + Path.explode("root-"+template+".tex"), directory.doc_dir+Path.explode("root.tex")) // copy Isabelle/DOF LaTeX styles - List(Path.explode("src/DOF/latex"), Path.explode("src/ontologies")) + List(Path.explode("DOF/latex"), Path.explode("ontologies")) .flatMap(dir => - File.find_files((dof_home + dir).file, + File.find_files((isabelle_dof_dir + dir).file, file => file.getName.endsWith(".sty"), include_dirs = true)) .foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file))