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

Adapted to Isabelle/1ac2416e8432 -- approx. Isabelle2022 release.

This commit is contained in:
Makarius Wenzel 2022-10-24 21:30:49 +02:00
parent 0aec98b95a
commit 0c8a0e1d63
6 changed files with 20 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -1183,7 +1183,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.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.presentation -> 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 ->
@ -1865,12 +1865,11 @@ Common Isar Syntax
\<^item>\<^ML>\<open>Args.name_position: (string * Position.T) parser\<close>
\<^item>\<^ML>\<open>Args.cartouche_inner_syntax: string parser\<close>
\<^item>\<^ML>\<open>Args.cartouche_input: Input.source parser\<close>
\<^item>\<^ML>\<open>Args.text_token: Token.T parser \<close>
Common Isar Syntax
\<^item>\<^ML>\<open>Args.text_input: Input.source parser\<close>
\<^item>\<^ML>\<open>Args.text : string parser\<close>
\<^item>\<^ML>\<open>Parse.embedded_input: Input.source parser\<close>
\<^item>\<^ML>\<open>Parse.embedded : string parser\<close>
\<^item>\<^ML>\<open>Args.binding : Binding.binding parser\<close>
Common Stuff related to Inner Syntax Parsing
@ -1893,8 +1892,7 @@ 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.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
\<^item>\<^ML>\<open>Args.embedded_declaration: (Input.source -> declaration) -> declaration 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>
@ -1903,8 +1901,6 @@ 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.text_declaration: (Input.source -> declaration) -> declaration parser\<close>
\<^item>\<^ML>\<open>Args.cartouche_declaration: (Input.source -> declaration) -> declaration parser\<close>
Syntax for some major Pure commands in Isar
\<^item>\<^ML>\<open>Args.prop: term context_parser\<close>

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>

8
src/DOF/Isa_DOF.thy
View File

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

2
src/DOF/RegExpInterface.thy
View File

@ -118,7 +118,7 @@ ML\<open>
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

14
src/scala/dof_document_build.scala
View File

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

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;