nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Merge branch 'makarius-isabelle_dev' into Isabelle_dev

This commit is contained in:
Achim D. Brucker 2022-10-30 11:53:13 +00:00
parent 0b807ea4bc cfdbd18bfa
commit f09a2df943
7 changed files with 25 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
etc/build.props
View File

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

2
src/DOF/Isa_COL.thy
View File

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

4
src/DOF/Isa_DOF.thy
View File

@ -2865,7 +2865,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;
@ -2881,7 +2881,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;

31
src/scala/dof_document_build.scala
View File

@ -28,10 +28,9 @@
* SPDX-License-Identifier: BSD-2-Clause
*/
package isabelle_dof
package isabelle.dof
import isabelle._
import java.io.{File => JFile}
object DOF_Document_Build
@ -50,31 +49,31 @@ 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 entry = context.session_context(name.theory, Export.DOCUMENT_LATEX + "_dof", permissive = true)
val xml = YXML.parse_body(entry.text)
if (xml.nonEmpty) {
File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic))
.write(directory.doc_dir)
}
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
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("DOF/latex"), Path.explode("ontologies"))
.flatMap(dir =>
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))
// create ontology.sty
val ltx_styles = context.options.string("dof_ontologies").split(" +").map(s => regex.replaceAllIn(s,""))

2
src/scala/dof_mkroot.scala
View File

@ -34,7 +34,7 @@
Prepare session root directory for Isabelle/DOF.
*/
package isabelle_dof
package isabelle.dof
import isabelle._

2
src/scala/dof_tools.scala
View File

@ -29,7 +29,7 @@
*/
package isabelle_dof
package isabelle.dof
import isabelle._

6
src/tests/OutOfOrderPresntn.thy
View File

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